# HG changeset patch
# User berghofe
# Date 1160755978 -7200
# Node ID e6b8d6784792207ffdc2aa8e645897935b4a5982
# Parent  5693e4471c2b22f9af6fce6fb701ced9d77b1f4f
Added new package for inductive definitions, moved old package
to old_inductive_package.ML

diff -r 5693e4471c2b -r e6b8d6784792 src/HOL/Inductive.thy
--- 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
diff -r 5693e4471c2b -r e6b8d6784792 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 13 18:10:16 2006 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 13 18:12:58 2006 +0200
@@ -106,7 +106,7 @@
   Tools/datatype_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.ML	\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
-  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
+  Tools/inductive_package.ML Tools/old_inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
   Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   Tools/polyhash.ML \
   Tools/recdef_package.ML Tools/recfun_codegen.ML				\