added helper -- cf. SET616^5
--- 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}]),
*)