# HG changeset patch
# User berghofe
# Date 1184144363 -7200
# Node ID 0e11b904b3a3b2e7596663e1c3bc4941ec92af9b
# Parent  3f8ad7418e55a2c91033beca09355eeb46404c55
Added new package for inductive sets.

diff -r 3f8ad7418e55 -r 0e11b904b3a3 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Jul 11 10:53:39 2007 +0200
+++ b/src/HOL/Inductive.thy	Wed Jul 11 10:59:23 2007 +0200
@@ -9,7 +9,7 @@
 imports FixedPoint Product_Type Sum_Type
 uses
   ("Tools/inductive_package.ML")
-  ("Tools/old_inductive_package.ML")
+  ("Tools/inductive_set_package.ML")
   ("Tools/inductive_realizer.ML")
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")
@@ -24,7 +24,7 @@
   ("Tools/primrec_package.ML")
 begin
 
-subsection {* Inductive sets *}
+subsection {* Inductive predicates and sets *}
 
 text {* Inversion of injective functions. *}
 
@@ -60,10 +60,7 @@
 
 text {* Package setup. *}
 
-ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *}
-setup OldInductivePackage.setup
-
-theorems basic_monos [mono] =
+theorems basic_monos =
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   Collect_mono in_mono vimage_mono
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
@@ -74,7 +71,7 @@
 use "Tools/inductive_package.ML"
 setup InductivePackage.setup
 
-theorems [mono2] =
+theorems [mono] =
   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
@@ -129,6 +126,9 @@
 
 use "Tools/primrec_package.ML"
 
+use "Tools/inductive_set_package.ML"
+setup InductiveSetPackage.setup
+
 text{* Lambda-abstractions with pattern matching: *}
 
 syntax
diff -r 3f8ad7418e55 -r 0e11b904b3a3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 11 10:53:39 2007 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 11 10:59:23 2007 +0200
@@ -117,10 +117,10 @@
   Tools/function_package/lexicographic_order.ML				\
   Tools/function_package/mutual.ML					\
   Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
-  Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML	\
+  Tools/inductive_package.ML Tools/inductive_realizer.ML		\
+  Tools/inductive_set_package.ML Tools/meson.ML				\
   Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
-  Tools/old_inductive_package.ML Tools/polyhash.ML 			\
-  Tools/primrec_package.ML Tools/prop_logic.ML 	\
+  Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML 	\
   Tools/recdef_package.ML Tools/recfun_codegen.ML			\
   Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML		\
   Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML	\