src/HOL/Recdef.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7357 d0e16da40ea2
child 7701 2c8c3b7003e5
permissions -rw-r--r--
tidied; added lemma restrict_to_left
wenzelm@5123
     1
wenzelm@7357
     2
theory Recdef = WF_Rel
wenzelm@7357
     3
files "Tools/recdef_package.ML" "Tools/induct_method.ML":
wenzelm@6438
     4
wenzelm@6438
     5
setup RecdefPackage.setup
wenzelm@6438
     6
setup InductMethod.setup
wenzelm@6438
     7
wenzelm@6438
     8
end