changeset 47944 | e6b51fab96f7 |
parent 47935 | 631ea563c20a |
child 47946 | 33afcfad3f8d |
--- 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}]), *)