author | nipkow |
Tue, 31 Mar 2015 17:29:44 +0200 | |
changeset 59864 | c777743294e1 |
parent 59863 | 30519ff3dffb |
child 59866 | eebe69f31474 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Tue Mar 31 15:01:06 2015 +0100 +++ b/src/HOL/HOL.thy Tue Mar 31 17:29:44 2015 +0200 @@ -1264,6 +1264,12 @@ then show "PROP P" . qed +lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" +by default (intro TrueI) + +lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True" +by default simp_all + lemma ex_simps: "!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)" "!!P Q. (EX x. P & Q x) = (P & (EX x. Q x))"