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

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

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

revision 2920 by nogin, Tue Feb 22 05:39:46 2000 UTC revision 2921 by steph, Mon Mar 13 23:03:12 2000 UTC
# Line 1123  Line 1123 
1123    
1124  module ITT_JProver = Jall.JProver(Itt_JLogic)  module ITT_JProver = Jall.JProver(Itt_JLogic)
1125    
1126  let jtest t s =  let jtest t s c = ITT_JProver.test t s c
1127   print_endline "Hello, I am";  
1128    ITT_JProver.test t s  
1129  let jprove = ITT_JProver.prove  let jprover t = ITT_JProver.prover t
1130    
1131    
1132    (* sequent calculus, another argumnet for proof reconstruction *)
1133    
1134  (*  (*
1135   * -*-   * -*-

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

  ViewVC Help
Powered by ViewVC 1.1.26