/[mojave]/metaprl/theories/itt/itt_logic.mli
ViewVC logotype

Diff of /metaprl/theories/itt/itt_logic.mli

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

revision 2920 by steph, Wed Feb 2 18:19:32 2000 UTC revision 2921 by steph, Mon Mar 13 23:03:12 2000 UTC
# Line 166  Line 166 
166  (************* jprover for itt_logic *************)  (************* jprover for itt_logic *************)
167    
168    
169  val jtest : Refiner.Refiner.TermSubst.term -> string -> unit  (* topval jtest : term -> string -> unit *)
170  val jprove : Refiner.Refiner.TermSubst.term ->  string ->  
171      (int * (string * string list) list) * (string * string) list * (string * string) list  topval jtest : term -> string -> string -> unit
172    
173    (* sequent calculus, another argumnet for proof reconstruction *)
174    
175    
176    val jprover : term -> (string * term * term) list
177    
178    
179    
 (* topval jprove : Refiner.Refiner.TermSubst.term ->  string ->  
     (int * (string * string list) list) * (string * string) list * (string * string) list  
 *)  
180    
181    
182  (*  (*

Legend:
Removed from v.2920  
changed lines
  Added in v.2921

  ViewVC Help
Powered by ViewVC 1.1.26