added Main.ML;

--- a/src/ZF/IsaMakefile	Sat Dec 08 16:13:20 2001 +0100
+++ b/src/ZF/IsaMakefile	Sat Dec 08 17:25:01 2001 +0100
@@ -28,29 +28,26 @@
 FOL:
 	@cd $(SRC)/FOL; $(ISATOOL) make FOL
 
-$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML           \
-  arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy                	\
-  Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy		\
-  Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML	\
-  Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
-  Inductive.thy InfDatatype.ML InfDatatype.thy \
-  Integ/Bin.ML Integ/Bin.thy \
-  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	Integ/Int.thy \
-  Integ/IntDiv.ML Integ/IntDiv.thy \
-  Integ/twos_compl.ML Integ/int_arith.ML Integ/IntArith.thy \
-  Let.ML Let.thy List.ML List.thy	\
-  Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
-  OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
-  Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
-  Rel.ML Rel.thy Sum.ML Sum.thy \
-  Tools/numeral_syntax.ML Tools/cartprod.ML				\
-  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
-  Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
+$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy ArithSimp.ML	\
+  ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
+  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy	\
+  Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy	\
+  Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy InfDatatype.ML	\
+  InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
+  Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
+  Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
+  Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
+  Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy	\
+  OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy Perm.ML Perm.thy	\
+  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
+  Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
+  Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
+  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
   Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
-  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy domrange.ML domrange.thy		\
-  equalities.ML equalities.thy func.ML func.thy ind_syntax.ML mono.ML	\
-  mono.thy pair.ML pair.thy simpdata.ML subset.ML subset.thy		\
-  thy_syntax.ML upair.ML upair.thy
+  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy arith_data.ML domrange.ML	\
+  domrange.thy equalities.ML equalities.thy func.ML func.thy		\
+  ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
+  subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
 	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Main.ML	Sat Dec 08 17:25:01 2001 +0100
@@ -0,0 +1,5 @@
+
+structure Main =
+struct
+  val thy = the_context ();
+end;