src/HOL/Inductive.thy
author wenzelm
Mon Oct 04 21:43:45 1999 +0200 (1999-10-04)
changeset 7700 38b6d2643630
parent 7357 d0e16da40ea2
child 7710 bf8cb3fc5d64
permissions -rw-r--r--
load / setup datatype package;
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@7700
     2
    ID:         $Id$
wenzelm@7700
     3
*)
lcp@1187
     4
wenzelm@7357
     5
theory Inductive = Gfp + Prod + Sum
wenzelm@7700
     6
files
wenzelm@7700
     7
  "Tools/inductive_package.ML"
wenzelm@7700
     8
  "Tools/datatype_aux.ML"
wenzelm@7700
     9
  "Tools/datatype_prop.ML"
wenzelm@7700
    10
  "Tools/datatype_rep_proofs.ML"
wenzelm@7700
    11
  "Tools/datatype_abs_proofs.ML"
wenzelm@7700
    12
  "Tools/datatype_package.ML"
wenzelm@7700
    13
  "Tools/primrec_package.ML":
wenzelm@6437
    14
wenzelm@6437
    15
setup InductivePackage.setup
wenzelm@7700
    16
setup DatatypePackage.setup
wenzelm@7700
    17
wenzelm@6437
    18
wenzelm@6437
    19
end