src/HOL/Inductive.thy
author wenzelm
Mon Oct 23 22:12:04 2000 +0200 (2000-10-23)
changeset 10312 4c5a03649af7
parent 10212 33fe2d701ddd
child 10402 5e82d6cafb5f
permissions -rw-r--r--
declare trancl rules;
     1 (*  Title:      HOL/Inductive.thy
     2     ID:         $Id$
     3 *)
     4 
     5 theory Inductive = Gfp + Sum_Type + NatDef
     6 files
     7   "Tools/induct_method.ML"
     8   "Tools/inductive_package.ML"
     9   "Tools/datatype_aux.ML"
    10   "Tools/datatype_prop.ML"
    11   "Tools/datatype_rep_proofs.ML"
    12   "Tools/datatype_abs_proofs.ML"
    13   "Tools/datatype_package.ML"
    14   "Tools/primrec_package.ML":
    15 
    16 setup InductMethod.setup
    17 setup InductivePackage.setup
    18 setup DatatypePackage.setup
    19 setup PrimrecPackage.setup
    20 
    21 theorems basic_monos [mono] =
    22    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
    23    Collect_mono in_mono vimage_mono
    24    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    25    not_all not_ex
    26    Ball_def Bex_def
    27 
    28 (*belongs to theory Transitive_Closure*)
    29 declare rtrancl_induct [induct set: rtrancl]
    30 declare rtranclE [cases set: rtrancl]
    31 declare trancl_induct [induct set: trancl]
    32 declare tranclE [cases set: trancl]
    33 
    34 end