src/HOL/Inductive.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7357 d0e16da40ea2
child 7700 38b6d2643630
permissions -rw-r--r--
tidied; added lemma restrict_to_left
lcp@1187
     1
wenzelm@7357
     2
theory Inductive = Gfp + Prod + Sum
wenzelm@7357
     3
files "Tools/inductive_package.ML":
wenzelm@6437
     4
wenzelm@6437
     5
setup InductivePackage.setup
wenzelm@6437
     6
wenzelm@6437
     7
end