src/ZF/ROOT.ML
changeset 12175 5cf58a1799a7
parent 12133 f314630235a4
child 12183 c10cea75dd56
     1.1 --- a/src/ZF/ROOT.ML	Tue Nov 13 22:20:15 2001 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Tue Nov 13 22:20:51 2001 +0100
     1.3 @@ -1,35 +1,29 @@
     1.4 -(*  Title:      ZF/ROOT
     1.5 +(*  Title:      ZF/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10 -Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
    1.11 -
    1.12 -This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
    1.13 +Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
    1.14 +This theory is the work of Martin Coen, Philippe Noel and Lawrence
    1.15 +Paulson.
    1.16  *)
    1.17  
    1.18  val banner = "ZF Set Theory (in FOL)";
    1.19  writeln banner;
    1.20  
    1.21 -eta_contract:=false;
    1.22 +reset eta_contract;
    1.23  
    1.24  print_depth 1;
    1.25  
    1.26 -(*Add user sections for inductive/datatype definitions*)
    1.27 -use     "thy_syntax";
    1.28 +(*syntax for old-style theory sections*)
    1.29 +use "thy_syntax";
    1.30  
    1.31  use "~~/src/Provers/Arith/cancel_numerals.ML";
    1.32  use "~~/src/Provers/Arith/combine_numerals.ML";
    1.33  
    1.34  use_thy "mono";
    1.35 -use     "ind_syntax.ML";
    1.36 -use     "Tools/cartprod.ML";
    1.37 -use_thy "Fixedpt";
    1.38 -use     "Tools/inductive_package.ML";
    1.39 -use     "Tools/induct_tacs.ML";
    1.40 -use     "Tools/primrec_package.ML";
    1.41 -use_thy "QUniv";
    1.42 -use     "Tools/datatype_package.ML";
    1.43 +use "ind_syntax.ML";
    1.44 +use_thy "Datatype";
    1.45  
    1.46  use     "Tools/numeral_syntax.ML";
    1.47  (*the all-in-one theory*)