NatSimprocs is now a theory, not a file
authorpaulson
Fri, 12 May 2000 15:05:02 +0200
changeset 8862 78643f8449c6
parent 8861 8341f24e09b5
child 8863 77245f4a71ef
NatSimprocs is now a theory, not a file
src/HOL/PreList.thy
--- 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