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;
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3 *)
     4 
     5 theory Inductive = Gfp + Prod + Sum
     6 files
     7   "Tools/inductive_package.ML"
     8   "Tools/datatype_aux.ML"
     9   "Tools/datatype_prop.ML"
    10   "Tools/datatype_rep_proofs.ML"
    11   "Tools/datatype_abs_proofs.ML"
    12   "Tools/datatype_package.ML"
    13   "Tools/primrec_package.ML":
    14 
    15 setup InductivePackage.setup
    16 setup DatatypePackage.setup
    17 
    18 
    19 end