/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

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

revision 3444 by nogin, Thu Nov 15 23:03:47 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 64  Line 64 
64  open Tactic_type.Tacticals  open Tactic_type.Tacticals
65  open Tactic_type.Conversionals  open Tactic_type.Conversionals
66    
67    (* XXX Bootstrapping HACK *)
68    let _ = Theory.substitute_dforms "comment" "summary"
69    
70  (************************************************************************  (************************************************************************
71   * TYPES                                                                *   * TYPES                                                                *
72   ************************************************************************)   ************************************************************************)

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

  ViewVC Help
Powered by ViewVC 1.1.26