# HG changeset patch
# User wenzelm
# Date 966501217 -7200
# Node ID 6125cc9efc185b76d8abac91d55e78560a11f2b2
# Parent  ff8238561394c4ebfb94988b55dcb7a8082240d6
fixed deps;

diff -r ff8238561394 -r 6125cc9efc18 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Aug 17 10:33:13 2000 +0200
+++ b/src/HOL/Main.thy	Thu Aug 17 10:33:37 2000 +0200
@@ -1,1 +1,5 @@
-Main = While + Map + String             (*theory Main includes everything*)
+
+(*theory Main includes everything; note that theory
+  PreList already includes most HOL theories*)
+
+Main = Map + String
diff -r ff8238561394 -r 6125cc9efc18 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Thu Aug 17 10:33:13 2000 +0200
+++ b/src/HOL/PreList.thy	Thu Aug 17 10:33:37 2000 +0200
@@ -9,7 +9,7 @@
 
 theory PreList =
   Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
-  SVC_Oracle:
+  SVC_Oracle + While:
 
 theorems [cases type: bool] = case_split