# HG changeset patch
# User paulson
# Date 956309298 -7200
# Node ID b03a0b21913966f054b8c448c9f5c2c27cc041a9
# Parent  8fdee31b795f38617cc4235af07d925c2410a5f8
new file Integ/NatSimprocs.ML

diff -r 8fdee31b795f -r b03a0b219139 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Fri Apr 21 11:27:28 2000 +0200
+++ b/src/HOL/PreList.thy	Fri Apr 21 11:28:18 2000 +0200
@@ -9,6 +9,7 @@
 
 theory PreList =
   Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
-  + SVC_Oracle:
+  + SVC_Oracle
+files "Integ/NatSimprocs.ML":
 
 end