/[mojave]/metaprl/refiner/reflib/jall.mli
ViewVC logotype

Diff of /metaprl/refiner/reflib/jall.mli

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

revision 2918 by steph, Wed Feb 2 18:19:32 2000 UTC revision 2919 by steph, Mon Mar 13 22:17:11 2000 UTC
# Line 8  Line 8 
8    
9  module JProver(JLogic: JLogicSig) :  module JProver(JLogic: JLogicSig) :
10  sig  sig
11    val test :  Refiner.Refiner.TermSubst.term -> string -> unit    val test :  Refiner.Refiner.Term.term -> string -> string -> unit  
12    val prove : Refiner.Refiner.TermSubst.term ->  string ->               (* sequent calculus, another argumnet for proof reconstruction *)
13      (int * (string * string list) list) * (string * string) list * (string * string) list    val prover :  Refiner.Refiner.Term.term -> (string * Refiner.Refiner.Term.term * Refiner.Refiner.Term.term) list
14  end  end
15    
16      
17    

Legend:
Removed from v.2918  
changed lines
  Added in v.2919

  ViewVC Help
Powered by ViewVC 1.1.26