src/HOL/Inductive.thy
author wenzelm
Sat Mar 04 13:25:09 2000 +0100 (2000-03-04)
changeset 8343 fb604f0e5640
parent 8303 5e7037409118
child 8482 bbc805ebc904
permissions -rw-r--r--
require NatDef;
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@7700
     2
    ID:         $Id$
wenzelm@7700
     3
*)
lcp@1187
     4
wenzelm@8343
     5
theory Inductive = Gfp + Prod + Sum + NatDef
wenzelm@7700
     6
files
wenzelm@8303
     7
  "Tools/induct_method.ML"
wenzelm@7700
     8
  "Tools/inductive_package.ML"
wenzelm@7700
     9
  "Tools/datatype_aux.ML"
wenzelm@7700
    10
  "Tools/datatype_prop.ML"
wenzelm@7700
    11
  "Tools/datatype_rep_proofs.ML"
wenzelm@7700
    12
  "Tools/datatype_abs_proofs.ML"
wenzelm@7700
    13
  "Tools/datatype_package.ML"
wenzelm@7700
    14
  "Tools/primrec_package.ML":
wenzelm@6437
    15
wenzelm@8303
    16
setup InductMethod.setup
wenzelm@6437
    17
setup InductivePackage.setup
wenzelm@7700
    18
setup DatatypePackage.setup
wenzelm@7700
    19
berghofe@7710
    20
theorems [mono] =
berghofe@7710
    21
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
berghofe@7710
    22
   Collect_mono in_mono vimage_mono
berghofe@7710
    23
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
berghofe@7710
    24
   not_all not_ex
berghofe@7710
    25
   Ball_def Bex_def
wenzelm@6437
    26
wenzelm@6437
    27
end