src/HOL/HOL.thy
changeset 60169 5ef8ed685965
parent 60151 9023d59acce6
child 60183 4cd4c204578c
     1.1 --- a/src/HOL/HOL.thy	Fri May 01 20:26:06 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun May 03 15:38:25 2015 +0200
     1.3 @@ -1270,6 +1270,10 @@
     1.4  lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
     1.5  by default simp_all
     1.6  
     1.7 +lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
     1.8 +  (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
     1.9 +by(rule swap_prems_eq)
    1.10 +
    1.11  lemma ex_simps:
    1.12    "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
    1.13    "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
    1.14 @@ -1293,7 +1297,7 @@
    1.15  lemmas [simp] =
    1.16    triv_forall_equality (*prunes params*)
    1.17    True_implies_equals implies_True_equals (*prune True in asms*)
    1.18 -  False_implies_equals (*prune False in asms*)
    1.19 +  False_implies_equals implies_False_swap (*prune False in asms*)
    1.20    if_True
    1.21    if_False
    1.22    if_cancel