src/HOL/HOL.thy
changeset 60151 9023d59acce6
parent 60147 6d7b7a037e8d
child 60169 5ef8ed685965
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 28 16:23:38 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 28 19:09:28 2015 +0200
     1.3 @@ -1270,10 +1270,6 @@
     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:
     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 @@ -1297,7 +1293,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 implies_False_swap (*prune False in asms*)
    1.19 +  False_implies_equals (*prune False in asms*)
    1.20    if_True
    1.21    if_False
    1.22    if_cancel