/[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 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC revision 2923 by lolorigo, Thu Mar 16 23:30:08 2000 UTC
# Line 1103  Line 1103 
1103    
1104  (************ logic instance for j-prover in refiner/reflib/jall.ml  **********)  (************ logic instance for j-prover in refiner/reflib/jall.ml  **********)
1105    
 open Nuprl5  
   
 module Nuprl_JLogic =  
 struct  
         let is_all_term = nuprl_is_all_term  
         let dest_all = nuprl_dest_all  
         let is_exists_term = nuprl_is_exists_term  
         let dest_exists = nuprl_dest_exists  
         let is_and_term = nuprl_is_and_term  
         let dest_and = nuprl_dest_and  
         let is_or_term = nuprl_is_or_term  
         let dest_or = nuprl_dest_or  
         let is_implies_term = nuprl_is_implies_term  
         let dest_implies = nuprl_dest_implies  
         let is_not_term = nuprl_is_not_term  
         let dest_not = nuprl_dest_not  
 end  
   
1106    
1107  module Itt_JLogic =  module Itt_JLogic =
1108  struct  struct
# Line 1139  Line 1121 
1121  end  end
1122    
1123    
1124  module ITT_JProver = Jall.JProver(Itt_JLogic) (* replace Itt_JLogic with Nuprl_JLogic for nv5 edd *)  module ITT_JProver = Jall.JProver(Itt_JLogic)
1125    
1126  let jtest t s c = ITT_JProver.test t s c  let jtest t s c = ITT_JProver.test t s c
1127    

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

  ViewVC Help
Powered by ViewVC 1.1.26