equal
deleted
inserted
replaced
62 |
62 |
63 use "Tools/old_inductive_package.ML" |
63 use "Tools/old_inductive_package.ML" |
64 setup OldInductivePackage.setup |
64 setup OldInductivePackage.setup |
65 |
65 |
66 theorems basic_monos [mono] = |
66 theorems basic_monos [mono] = |
67 subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2 |
67 subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
68 Collect_mono in_mono vimage_mono |
68 Collect_mono in_mono vimage_mono |
69 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
69 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
70 not_all not_ex |
70 not_all not_ex |
71 Ball_def Bex_def |
71 Ball_def Bex_def |
72 induct_rulify_fallback |
72 induct_rulify_fallback |
73 |
73 |
74 use "Tools/inductive_package.ML" |
74 use "Tools/inductive_package.ML" |
75 setup InductivePackage.setup |
75 setup InductivePackage.setup |
76 |
76 |
77 theorems [mono2] = |
77 theorems [mono2] = |
78 imp_refl disj_mono conj_mono ex_mono all_mono if_def2 |
78 imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj |
79 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
79 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
80 not_all not_ex |
80 not_all not_ex |
81 Ball_def Bex_def |
81 Ball_def Bex_def |
82 induct_rulify_fallback |
82 induct_rulify_fallback |
83 |
83 |