1644 (("COMBK", false), @{thms Meson.COMBK_def}), |
1644 (("COMBK", false), @{thms Meson.COMBK_def}), |
1645 (("COMBB", false), @{thms Meson.COMBB_def}), |
1645 (("COMBB", false), @{thms Meson.COMBB_def}), |
1646 (("COMBC", false), @{thms Meson.COMBC_def}), |
1646 (("COMBC", false), @{thms Meson.COMBC_def}), |
1647 (("COMBS", false), @{thms Meson.COMBS_def}), |
1647 (("COMBS", false), @{thms Meson.COMBS_def}), |
1648 ((predicator_name, false), [not_ffalse, ftrue]), |
1648 ((predicator_name, false), [not_ffalse, ftrue]), |
|
1649 ((predicator_name, true), @{thms True_or_False}), |
1649 (* FIXME: Metis doesn't like existentials in helpers |
1650 (* FIXME: Metis doesn't like existentials in helpers |
1650 ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]), |
1651 ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]), |
1651 *) |
1652 *) |
1652 (("fFalse", false), [not_ffalse]), |
1653 (("fFalse", false), [not_ffalse]), |
1653 (("fFalse", true), @{thms True_or_False}), |
1654 (("fFalse", true), @{thms True_or_False}), |