src/HOL/Tools/Metis/metis_tactics.ML
changeset 43299 f78d5f0818a0
parent 43298 82d4874757df
child 43301 8d7fc4a5b502
equal deleted inserted replaced
43298:82d4874757df 43299:f78d5f0818a0
   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