# HG changeset patch
# User wenzelm
# Date 966614029 -7200
# Node ID 6f0b89f2a1f9153fa645c4ac3e6334f3203dde16
# Parent  89155e48fa53c6cff284facdc51df40169e9f598
Main now new-style theory; added Main.ML for compatibility;

diff -r 89155e48fa53 -r 6f0b89f2a1f9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 18 12:34:48 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 18 17:53:49 2000 +0200
@@ -57,7 +57,7 @@
   Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
   Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
-  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML        \
+  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
   Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
   Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
diff -r 89155e48fa53 -r 6f0b89f2a1f9 src/HOL/Main.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Main.ML	Fri Aug 18 17:53:49 2000 +0200
@@ -0,0 +1,5 @@
+
+structure Main =
+struct
+  val thy = the_context ();
+end;
diff -r 89155e48fa53 -r 6f0b89f2a1f9 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Aug 18 12:34:48 2000 +0200
+++ b/src/HOL/Main.thy	Fri Aug 18 17:53:49 2000 +0200
@@ -2,4 +2,7 @@
 (*theory Main includes everything; note that theory
   PreList already includes most HOL theories*)
 
-Main = Map + String
+theory Main = Map + String:
+
+end
+