src/HOL/Recdef.thy
changeset 7357 d0e16da40ea2
parent 6438 e55a1869ed38
child 7701 2c8c3b7003e5
--- a/src/HOL/Recdef.thy	Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/Recdef.thy	Wed Aug 25 20:49:02 1999 +0200
@@ -1,5 +1,6 @@
 
-Recdef = WF_Rel +
+theory Recdef = WF_Rel
+files "Tools/recdef_package.ML" "Tools/induct_method.ML":
 
 setup RecdefPackage.setup
 setup InductMethod.setup