--- a/src/HOL/Extraction.thy Tue Apr 28 16:23:38 2015 +0100
+++ b/src/HOL/Extraction.thy Tue Apr 28 19:09:28 2015 +0200
@@ -32,7 +32,7 @@
induct_atomize induct_atomize' induct_rulify induct_rulify'
induct_rulify_fallback induct_trueI
True_implies_equals implies_True_equals TrueE
- False_implies_equals implies_False_swap
+ False_implies_equals
lemmas [extraction_expand_def] =
HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
--- a/src/HOL/HOL.thy Tue Apr 28 16:23:38 2015 +0100
+++ b/src/HOL/HOL.thy Tue Apr 28 19:09:28 2015 +0200
@@ -1270,10 +1270,6 @@
lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
by default simp_all
-lemma implies_False_swap:
- "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
-by(rule swap_prems_eq)
-
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))"
@@ -1297,7 +1293,7 @@
lemmas [simp] =
triv_forall_equality (*prunes params*)
True_implies_equals implies_True_equals (*prune True in asms*)
- False_implies_equals implies_False_swap (*prune False in asms*)
+ False_implies_equals (*prune False in asms*)
if_True
if_False
if_cancel
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Tue Apr 28 16:23:38 2015 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Tue Apr 28 19:09:28 2015 +0200
@@ -192,7 +192,6 @@
--\<open>6 subgoals left\<close>
prefer 6
apply(erule_tac x=i in allE)
-apply simp
apply fastforce
--\<open>5 subgoals left\<close>
prefer 5