/[mojave]/metaprl/editor/ml/nuprl_jprover.mli
ViewVC logotype

Diff of /metaprl/editor/ml/nuprl_jprover.mli

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC revision 2923 by lolorigo, Thu Mar 16 23:30:08 2000 UTC
# Line 27  Line 27 
27   *         *      
28   *)   *)
29    
30  val jprover_result_to_term : (string * Refiner.Refiner.Term.term * Refiner.Refiner.Term.term) list -> Refiner.Refiner.Term.term  open Refiner.Refiner.Term
31    
32    val jprover_result_to_term : (string * term * term) list -> term
33    
34    (* sequent calculus, another argument for proof reconstruction *)
35    
36    val jprover : term -> (string * term * term) list
37    
38    

Legend:
Removed from v.2922  
changed lines
  Added in v.2923

  ViewVC Help
Powered by ViewVC 1.1.26