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