Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
authorblanchet
Wed, 16 May 2012 18:16:51 +0200
changeset 47935 631ea563c20a
parent 47934 08d7aff8c7e6
child 47936 756f30eac792
temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
src/HOL/Tools/ATP/atp_problem_generate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
@@ -1646,8 +1646,9 @@
    (("COMBC", false), @{thms Meson.COMBC_def}),
    (("COMBS", false), @{thms Meson.COMBS_def}),
    ((predicator_name, false), [not_ffalse, ftrue]),
-   (* FIXME: Metis doesn't like existentials in helpers *)
+(* FIXME: Metis doesn't like existentials in helpers
    ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
+*)
    (("fFalse", false), [not_ffalse]),
    (("fFalse", true), @{thms True_or_False}),
    (("fTrue", false), [ftrue]),
isabelle