temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
authorblanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 47935631ea563c20a
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
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -1646,8 +1646,9 @@
     1.4     (("COMBC", false), @{thms Meson.COMBC_def}),
     1.5     (("COMBS", false), @{thms Meson.COMBS_def}),
     1.6     ((predicator_name, false), [not_ffalse, ftrue]),
     1.7 -   (* FIXME: Metis doesn't like existentials in helpers *)
     1.8 +(* FIXME: Metis doesn't like existentials in helpers
     1.9     ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
    1.10 +*)
    1.11     (("fFalse", false), [not_ffalse]),
    1.12     (("fFalse", true), @{thms True_or_False}),
    1.13     (("fTrue", false), [ftrue]),