| changeset 11003 | ee0838d89deb |
| parent 10727 | 2ccafccb81c0 |
| child 11325 | a5e0289dd56c |
--- a/src/HOL/Inductive.thy Tue Jan 30 18:53:46 2001 +0100 +++ b/src/HOL/Inductive.thy Tue Jan 30 18:57:24 2001 +0100 @@ -75,7 +75,7 @@ setup PrimrecPackage.setup theorems basic_monos [mono] = - subset_refl imp_refl disj_mono conj_mono ex_mono all_mono + subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 Collect_mono in_mono vimage_mono imp_conv_disj not_not de_Morgan_disj de_Morgan_conj not_all not_ex