src/HOL/PreList.thy
changeset 8840 18b76c137c41
parent 8756 b03a0b219139
child 8862 78643f8449c6
--- a/src/HOL/PreList.thy	Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/PreList.thy	Mon May 08 20:59:30 2000 +0200
@@ -8,8 +8,7 @@
 *)
 
 theory PreList =
-  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
-  + SVC_Oracle
+  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
 files "Integ/NatSimprocs.ML":
 
 end