equal
deleted
inserted
replaced
140 #> Meson.finish_cnf |
140 #> Meson.finish_cnf |
141 |
141 |
142 fun preskolem_tac ctxt st0 = |
142 fun preskolem_tac ctxt st0 = |
143 (if exists (Meson.has_too_many_clauses ctxt) |
143 (if exists (Meson.has_too_many_clauses ctxt) |
144 (Logic.prems_of_goal (prop_of st0) 1) then |
144 (Logic.prems_of_goal (prop_of st0) 1) then |
145 cnf.cnfx_rewrite_tac ctxt 1 |
145 Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 |
|
146 THEN cnf.cnfx_rewrite_tac ctxt 1 |
146 else |
147 else |
147 all_tac) st0 |
148 all_tac) st0 |
148 |
149 |
149 val type_has_top_sort = |
150 val type_has_top_sort = |
150 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
151 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |