Added new package for inductive sets.
--- 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
--- 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 \