# HG changeset patch
# User nipkow
# Date 1430660305 -7200
# Node ID 5ef8ed6859659510fd5420a6af5859bc422effb4
# Parent  0305c511a8211276891cc58839a044a9df023771
swap False to the right in assumptions to be eliminated at the right end

diff -r 0305c511a821 -r 5ef8ed685965 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Fri May 01 20:26:06 2015 +0200
+++ b/src/HOL/Extraction.thy	Sun May 03 15:38:25 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
+  False_implies_equals implies_False_swap
 
 lemmas [extraction_expand_def] =
   HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
diff -r 0305c511a821 -r 5ef8ed685965 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri May 01 20:26:06 2015 +0200
+++ b/src/HOL/HOL.thy	Sun May 03 15:38:25 2015 +0200
@@ -1270,6 +1270,10 @@
 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
 by default simp_all
 
+lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
+  (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))"
@@ -1293,7 +1297,7 @@
 lemmas [simp] =
   triv_forall_equality (*prunes params*)
   True_implies_equals implies_True_equals (*prune True in asms*)
-  False_implies_equals (*prune False in asms*)
+  False_implies_equals implies_False_swap (*prune False in asms*)
   if_True
   if_False
   if_cancel
diff -r 0305c511a821 -r 5ef8ed685965 src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Fri May 01 20:26:06 2015 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun May 03 15:38:25 2015 +0200
@@ -191,7 +191,7 @@
 apply force
 --\<open>6 subgoals left\<close>
 prefer 6
-apply(erule_tac x=i in allE)
+apply(erule_tac x=j in allE)
 apply fastforce
 --\<open>5 subgoals left\<close>
 prefer 5