src/HOL/PreList.thy
changeset 8862 78643f8449c6
parent 8840 18b76c137c41
child 9066 b1e874e38dab
--- a/src/HOL/PreList.thy	Fri May 12 15:02:57 2000 +0200
+++ b/src/HOL/PreList.thy	Fri May 12 15:05:02 2000 +0200
@@ -8,7 +8,7 @@
 *)
 
 theory PreList =
-  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
-files "Integ/NatSimprocs.ML":
+  Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
+  SVC_Oracle:
 
 end