# HG changeset patch
# User paulson
# Date 958136702 -7200
# Node ID 78643f8449c66dd79b7809574f5051e8a50bd490
# Parent  8341f24e09b514a958ac0189b3ded931cb701da7
NatSimprocs is now a theory, not a file

diff -r 8341f24e09b5 -r 78643f8449c6 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