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

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

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

revision 3583 by jyh, Wed Jun 23 04:50:29 1999 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 46  Line 46 
46  (* Save the theory *)  (* Save the theory *)
47  val record_theory : theory -> unit  val record_theory : theory -> unit
48    
49    (* XXX: bootstrapping HACK:
50     * replace the dforms in a theory with something more complete *)
51    val substitute_dforms : string -> string -> unit
52    
53  (* Get back all the theories that have been recorded *)  (* Get back all the theories that have been recorded *)
54  val get_theories : unit -> theory list  val get_theories : unit -> theory list
55    

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26