Added new package for inductive definitions, moved old package
authorberghofe
Fri Oct 13 18:12:58 2006 +0200 (2006-10-13)
changeset 21018e6b8d6784792
parent 21017 5693e4471c2b
child 21019 650c48711c7b
Added new package for inductive definitions, moved old package
to old_inductive_package.ML
src/HOL/Inductive.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Inductive.thy	Fri Oct 13 18:10:16 2006 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Oct 13 18:12:58 2006 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  imports FixedPoint Sum_Type Relation Record
     1.5  uses
     1.6    ("Tools/inductive_package.ML")
     1.7 +  ("Tools/old_inductive_package.ML")
     1.8    ("Tools/inductive_realizer.ML")
     1.9    ("Tools/inductive_codegen.ML")
    1.10    ("Tools/datatype_aux.ML")
    1.11 @@ -59,8 +60,8 @@
    1.12  
    1.13  text {* Package setup. *}
    1.14  
    1.15 -use "Tools/inductive_package.ML"
    1.16 -setup InductivePackage.setup
    1.17 +use "Tools/old_inductive_package.ML"
    1.18 +setup OldInductivePackage.setup
    1.19  
    1.20  theorems basic_monos [mono] =
    1.21    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    1.22 @@ -70,6 +71,16 @@
    1.23    Ball_def Bex_def
    1.24    induct_rulify_fallback
    1.25  
    1.26 +use "Tools/inductive_package.ML"
    1.27 +setup InductivePackage.setup
    1.28 +
    1.29 +theorems [mono2] =
    1.30 +  imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    1.31 +  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.32 +  not_all not_ex
    1.33 +  Ball_def Bex_def
    1.34 +  induct_rulify_fallback
    1.35 +
    1.36  lemma False_meta_all:
    1.37    "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
    1.38  proof
     2.1 --- a/src/HOL/IsaMakefile	Fri Oct 13 18:10:16 2006 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 13 18:12:58 2006 +0200
     2.3 @@ -106,7 +106,7 @@
     2.4    Tools/datatype_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.ML	\
     2.5    Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
     2.6    Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
     2.7 -  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
     2.8 +  Tools/inductive_package.ML Tools/old_inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
     2.9    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
    2.10    Tools/polyhash.ML \
    2.11    Tools/recdef_package.ML Tools/recfun_codegen.ML				\