equal
deleted
inserted
replaced
205 "Metis called with theorems\n" ^ |
205 "Metis called with theorems\n" ^ |
206 cat_lines (map (Display.string_of_thm ctxt) ths)) |
206 cat_lines (map (Display.string_of_thm ctxt) ths)) |
207 fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 |
207 fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 |
208 in |
208 in |
209 if exists_type type_has_top_sort (prop_of st0) then |
209 if exists_type type_has_top_sort (prop_of st0) then |
210 (verbose_warning ctxt "Proof state contains the universal sort {}"; |
210 verbose_warning ctxt "Proof state contains the universal sort {}" |
211 Seq.empty) |
|
212 else |
211 else |
213 Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 |
212 (); |
|
213 Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 |
214 end |
214 end |
215 |
215 |
216 val metis_default_type_syss = [partial_type_sys, full_type_sys] |
216 val metis_default_type_syss = [partial_type_sys, full_type_sys] |
217 val metisFT_type_syss = [full_type_sys] |
217 val metisFT_type_syss = [full_type_sys] |
218 |
218 |