Streamlined setup for monotonicity rules (no longer requires classical rules).
authorberghofe
Fri Nov 27 16:26:04 2009 +0100 (2009-11-27)
changeset 3393425d6a8982e37
parent 33933 e429668becc1
child 33935 b94b4587106a
Streamlined setup for monotonicity rules (no longer requires classical rules).
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Fri Nov 27 16:24:31 2009 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Nov 27 16:26:04 2009 +0100
     1.3 @@ -262,18 +262,13 @@
     1.4  theorems basic_monos =
     1.5    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     1.6    Collect_mono in_mono vimage_mono
     1.7 -  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
     1.8 -  not_all not_ex
     1.9 -  Ball_def Bex_def
    1.10 -  induct_rulify_fallback
    1.11  
    1.12  use "Tools/inductive.ML"
    1.13  setup Inductive.setup
    1.14  
    1.15  theorems [mono] =
    1.16    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.17 -  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.18 -  not_all not_ex
    1.19 +  imp_mono not_mono
    1.20    Ball_def Bex_def
    1.21    induct_rulify_fallback
    1.22