| changeset 58817 | 4cd778c91fdc |
| parent 54553 | 2b0da4c1dd40 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Meson.thy Wed Oct 29 13:42:38 2014 +0100 +++ b/src/HOL/Meson.thy Wed Oct 29 13:57:20 2014 +0100 @@ -195,8 +195,6 @@ ML_file "Tools/Meson/meson_clausify.ML" ML_file "Tools/Meson/meson_tactic.ML" -setup {* Meson_Tactic.setup *} - hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD