added helper -- cf. SET616^5
authorblanchet
Mon, 21 May 2012 10:39:31 +0200
changeset 47944 e6b51fab96f7
parent 47943 c09326cedb41
child 47945 4073e51293cf
added helper -- cf. SET616^5
src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri May 18 17:36:20 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 10:39:31 2012 +0200
@@ -1646,6 +1646,7 @@
    (("COMBC", false), @{thms Meson.COMBC_def}),
    (("COMBS", false), @{thms Meson.COMBS_def}),
    ((predicator_name, false), [not_ffalse, ftrue]),
+   ((predicator_name, true), @{thms True_or_False}),
 (* FIXME: Metis doesn't like existentials in helpers
    ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
 *)