src/HOL/Inductive.thy
changeset 23734 0e11b904b3a3
parent 23708 b5eb0b4dd17d
child 24349 0dd8782fb02d
     1.1 --- a/src/HOL/Inductive.thy	Wed Jul 11 10:53:39 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Jul 11 10:59:23 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports FixedPoint Product_Type Sum_Type
     1.5  uses
     1.6    ("Tools/inductive_package.ML")
     1.7 -  ("Tools/old_inductive_package.ML")
     1.8 +  ("Tools/inductive_set_package.ML")
     1.9    ("Tools/inductive_realizer.ML")
    1.10    ("Tools/inductive_codegen.ML")
    1.11    ("Tools/datatype_aux.ML")
    1.12 @@ -24,7 +24,7 @@
    1.13    ("Tools/primrec_package.ML")
    1.14  begin
    1.15  
    1.16 -subsection {* Inductive sets *}
    1.17 +subsection {* Inductive predicates and sets *}
    1.18  
    1.19  text {* Inversion of injective functions. *}
    1.20  
    1.21 @@ -60,10 +60,7 @@
    1.22  
    1.23  text {* Package setup. *}
    1.24  
    1.25 -ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *}
    1.26 -setup OldInductivePackage.setup
    1.27 -
    1.28 -theorems basic_monos [mono] =
    1.29 +theorems basic_monos =
    1.30    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.31    Collect_mono in_mono vimage_mono
    1.32    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.33 @@ -74,7 +71,7 @@
    1.34  use "Tools/inductive_package.ML"
    1.35  setup InductivePackage.setup
    1.36  
    1.37 -theorems [mono2] =
    1.38 +theorems [mono] =
    1.39    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.40    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.41    not_all not_ex
    1.42 @@ -129,6 +126,9 @@
    1.43  
    1.44  use "Tools/primrec_package.ML"
    1.45  
    1.46 +use "Tools/inductive_set_package.ML"
    1.47 +setup InductiveSetPackage.setup
    1.48 +
    1.49  text{* Lambda-abstractions with pattern matching: *}
    1.50  
    1.51  syntax