src/HOL/Recdef.thy
changeset 7357 d0e16da40ea2
parent 6438 e55a1869ed38
child 7701 2c8c3b7003e5
equal deleted inserted replaced
7356:1714c91b8729 7357:d0e16da40ea2
     1 
     1 
     2 Recdef = WF_Rel +
     2 theory Recdef = WF_Rel
       
     3 files "Tools/recdef_package.ML" "Tools/induct_method.ML":
     3 
     4 
     4 setup RecdefPackage.setup
     5 setup RecdefPackage.setup
     5 setup InductMethod.setup
     6 setup InductMethod.setup
     6 
     7 
     7 end
     8 end