src/HOL/Inductive.thy
changeset 22218 30a8890d2967
parent 21018 e6b8d6784792
child 22783 e5f947e0ade8
     1.1 --- a/src/HOL/Inductive.thy	Wed Jan 31 14:03:31 2007 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Jan 31 16:05:10 2007 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  setup OldInductivePackage.setup
     1.5  
     1.6  theorems basic_monos [mono] =
     1.7 -  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
     1.8 +  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     1.9    Collect_mono in_mono vimage_mono
    1.10    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.11    not_all not_ex
    1.12 @@ -75,7 +75,7 @@
    1.13  setup InductivePackage.setup
    1.14  
    1.15  theorems [mono2] =
    1.16 -  imp_refl disj_mono conj_mono ex_mono all_mono if_def2
    1.17 +  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.18    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.19    not_all not_ex
    1.20    Ball_def Bex_def