/[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 2921 by steph, Mon Mar 13 23:03:12 2000 UTC revision 2922 by lolorigo, Thu Mar 16 19:52:02 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    
1106    open Nuprl5
1107    
1108    module Nuprl_JLogic =
1109    struct
1110            let is_all_term = nuprl_is_all_term
1111            let dest_all = nuprl_dest_all
1112            let is_exists_term = nuprl_is_exists_term
1113            let dest_exists = nuprl_dest_exists
1114            let is_and_term = nuprl_is_and_term
1115            let dest_and = nuprl_dest_and
1116            let is_or_term = nuprl_is_or_term
1117            let dest_or = nuprl_dest_or
1118            let is_implies_term = nuprl_is_implies_term
1119            let dest_implies = nuprl_dest_implies
1120            let is_not_term = nuprl_is_not_term
1121            let dest_not = nuprl_dest_not
1122    end
1123    
1124    
1125  module Itt_JLogic =  module Itt_JLogic =
1126  struct  struct
# Line 1121  Line 1139 
1139  end  end
1140    
1141    
1142  module ITT_JProver = Jall.JProver(Itt_JLogic)  module ITT_JProver = Jall.JProver(Itt_JLogic) (* replace Itt_JLogic with Nuprl_JLogic for nv5 edd *)
1143    
1144  let jtest t s c = ITT_JProver.test t s c  let jtest t s c = ITT_JProver.test t s c
1145    

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

  ViewVC Help
Powered by ViewVC 1.1.26