src/HOL/Inductive.thy

 
 theory Inductive 
 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")
   ("Tools/datatype_prop.ML")
   ("Tools/datatype_rep_proofs.ML")

   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
   ("Tools/primrec_package.ML")
 begin
 
-subsection {* Inductive sets *}
+subsection {* Inductive predicates and sets *}
 
 text {* Inversion of injective functions. *}
 
 constdefs
   myinv :: "('a => 'b) => ('b => 'a)"

 hide const myinv
 
 
 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
   not_all not_ex
   Ball_def Bex_def
   induct_rulify_fallback
 
 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
   Ball_def Bex_def
   induct_rulify_fallback

 use "Tools/inductive_codegen.ML"
 setup InductiveCodegen.setup
 
 use "Tools/primrec_package.ML"
 
+use "Tools/inductive_set_package.ML"
+setup InductiveSetPackage.setup
+
 text{* Lambda-abstractions with pattern matching: *}
 
 syntax
   "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
 syntax (xsymbols)