# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1427816981 -3600
# Node ID eebe69f314746aaf36d1d8b8d7b332e03bbcfb34
# Parent  8a20dd967385afb2917e0b3d9b85da119e07d4ff# Parent  c777743294e100250c24a4ecea97594e5e63f3da
Merge

diff -r 8a20dd967385 -r eebe69f31474 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Mar 31 16:48:48 2015 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 31 16:49:41 2015 +0100
@@ -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))"