Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 39038 dfea12cc5f5a
parent 39037 5146d640aa4a
child 39112 611e41ef07c3 
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 02 13:18:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 02 13:45:23 2010 +0200
@@ -802,7 +802,7 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Meson.MESON (K all_tac) (* FIXME: Try (cnf.cnfx_rewrite_tac ctxt) *)
+      Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
                   (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
isabelle