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

Diff of /metaprl/editor/ml/nuprl_jprover.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 28  Line 28 
28    
29  open Refiner.Refiner.Term  open Refiner.Refiner.Term
30  open Refiner.Refiner.TermType  open Refiner.Refiner.TermType
31    open Nuprl5
32    
33    module Nuprl_JLogic =
34    struct
35            let is_all_term = nuprl_is_all_term
36            let dest_all = nuprl_dest_all
37            let is_exists_term = nuprl_is_exists_term
38            let dest_exists = nuprl_dest_exists
39            let is_and_term = nuprl_is_and_term
40            let dest_and = nuprl_dest_and
41            let is_or_term = nuprl_is_or_term
42            let dest_or = nuprl_dest_or
43            let is_implies_term = nuprl_is_implies_term
44            let dest_implies = nuprl_dest_implies
45            let is_not_term = nuprl_is_not_term
46            let dest_not = nuprl_dest_not
47    end
48    
49    
50    module Nuprl_JProver = Jall.JProver(Nuprl_JLogic)
51    
52    let jprover t = Nuprl_JProver.prover t
53    
54    
55  (* jprover fun returns string*term*term list, convert to term *)  (* jprover fun returns string*term*term list, convert to term *)
56    

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

  ViewVC Help
Powered by ViewVC 1.1.26