src/HOL/HOL.thy
changeset 59864 c777743294e1
parent 59779 b6bda9140e39
child 59929 a090551e5ec8
     1.1 --- a/src/HOL/HOL.thy	Tue Mar 31 15:01:06 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Mar 31 17:29:44 2015 +0200
     1.3 @@ -1264,6 +1264,12 @@
     1.4    then show "PROP P" .
     1.5  qed
     1.6  
     1.7 +lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
     1.8 +by default (intro TrueI)
     1.9 +
    1.10 +lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
    1.11 +by default simp_all
    1.12 +
    1.13  lemma ex_simps:
    1.14    "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
    1.15    "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"