--- a/ROOT.ML Thu Aug 25 10:47:33 1994 +0200
+++ b/ROOT.ML Thu Aug 25 11:01:45 1994 +0200
@@ -10,13 +10,7 @@
val banner = "Higher-Order Logic";
writeln banner;
-(* Add user section "datatype" *)
-use "Datatype.ML";
-structure ThySyn =
- ThySynFun(val user_keywords = ["|", "datatype", "primrec"]
- and user_sections = [("datatype", datatype_decls),
- ("primrec", primrec_decl)]);
-init_thy_reader ();
+init_thy_reader();
print_depth 1;
eta_contract := true;
@@ -81,6 +75,29 @@
use_thy "equalities";
use_thy "Prod";
use_thy "Sum";
+use_thy "Gfp";
+use_thy "Nat";
+
+(* Add user sections *)
+use "Datatype.ML";
+use "../Pure/section_utils.ML";
+use "ind_syntax.ML";
+use "add_ind_def.ML";
+use "intr_elim.ML";
+use "indrule.ML";
+use "Inductive.ML";
+
+structure ThySyn = ThySynFun
+ (val user_keywords = ["|", "datatype", "primrec",
+ "inductive", "coinductive", "intrs",
+ "monos", "con_defs"]
+ and user_sections = [("inductive", inductive_decl ""),
+ ("coinductive", inductive_decl "Co"),
+ ("datatype", datatype_decls),
+ ("primrec", primrec_decl)]);
+init_thy_reader ();
+
+use_thy "Finite";
use_thy "LList";
use "../Pure/install_pp.ML";