# HG changeset patch
# User blanchet
# Date 1337589571 -7200
# Node ID e6b51fab96f796331a70c05adb526dfe95cf9af0
# Parent  c09326cedb4158315a93ddf71ed2dc8ac18661d4
added helper -- cf. SET616^5

diff -r c09326cedb41 -r e6b51fab96f7 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}]),
 *)