src/HOLCF/ROOT.ML
changeset 3623 e843c1d6f9e1
parent 3608 d81caea336ba
child 3953 473ea5ce5ca8
     1.1 --- a/src/HOLCF/ROOT.ML	Wed Aug 06 11:57:52 1997 +0200
     1.2 +++ b/src/HOLCF/ROOT.ML	Wed Aug 06 11:58:50 1997 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOLCF/ROOT
     1.5 +(*  Title:      HOLCF/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8      Copyright   1993 Technische Universitaet Muenchen
     1.9 @@ -7,14 +7,15 @@
    1.10  Should be executed in subdirectory HOLCF.
    1.11  *)
    1.12  
    1.13 -val banner = "HOLCF with sections axioms,ops,domain,generated";
    1.14 +val banner = "HOLCF";
    1.15  writeln banner;
    1.16  
    1.17  print_depth 1;
    1.18  
    1.19  use_thy "HOLCF";
    1.20  
    1.21 -(* install sections: axioms, ops *)
    1.22 +
    1.23 +(* sections axioms, ops *)
    1.24  
    1.25  use "ax_ops/holcflogic.ML";
    1.26  use "ax_ops/thy_axioms.ML";
    1.27 @@ -22,7 +23,7 @@
    1.28  use "ax_ops/thy_syntax.ML";
    1.29  
    1.30  
    1.31 -(* install sections: domain, generated *)
    1.32 +(* sections domain, generated *)
    1.33  
    1.34  use "domain/library.ML";
    1.35  use "domain/syntax.ML";
    1.36 @@ -31,11 +32,6 @@
    1.37  use "domain/extender.ML";
    1.38  use "domain/interface.ML";
    1.39  
    1.40 -set_parser ThySyn.parse;
    1.41 -
    1.42 -fun qed_spec_mp name =
    1.43 -  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.44 -  in bind_thm(name, thm) end;
    1.45  
    1.46  print_depth 10;  
    1.47