--- a/src/HOL/Inductive.thy Fri Oct 13 18:10:16 2006 +0200
+++ b/src/HOL/Inductive.thy Fri Oct 13 18:12:58 2006 +0200
@@ -9,6 +9,7 @@
imports FixedPoint Sum_Type Relation Record
uses
("Tools/inductive_package.ML")
+ ("Tools/old_inductive_package.ML")
("Tools/inductive_realizer.ML")
("Tools/inductive_codegen.ML")
("Tools/datatype_aux.ML")
@@ -59,8 +60,8 @@
text {* Package setup. *}
-use "Tools/inductive_package.ML"
-setup InductivePackage.setup
+use "Tools/old_inductive_package.ML"
+setup OldInductivePackage.setup
theorems basic_monos [mono] =
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
@@ -70,6 +71,16 @@
Ball_def Bex_def
induct_rulify_fallback
+use "Tools/inductive_package.ML"
+setup InductivePackage.setup
+
+theorems [mono2] =
+ imp_refl disj_mono conj_mono ex_mono all_mono if_def2
+ imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
+ not_all not_ex
+ Ball_def Bex_def
+ induct_rulify_fallback
+
lemma False_meta_all:
"Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
proof