equal
deleted
inserted
replaced
190 |
190 |
191 use "Tools/Meson/meson.ML" |
191 use "Tools/Meson/meson.ML" |
192 use "Tools/Meson/meson_clausify.ML" |
192 use "Tools/Meson/meson_clausify.ML" |
193 use "Tools/Meson/meson_tactic.ML" |
193 use "Tools/Meson/meson_tactic.ML" |
194 |
194 |
195 setup {* |
195 setup {* Meson_Tactic.setup *} |
196 Meson.setup |
|
197 #> Meson_Tactic.setup |
|
198 *} |
|
199 |
196 |
200 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem |
197 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem |
201 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD |
198 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD |
202 not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD |
199 not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD |
203 disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI |
200 disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI |