# HG changeset patch
# User nipkow
# Date 1431166764 -7200
# Node ID 4cd4c204578c9642a241e29bbd2e035762b29dba
# Parent  e1ea5a6379c927760ab79ba8e56ddf3163cb4ec5
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)

diff -r e1ea5a6379c9 -r 4cd4c204578c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu May 07 15:34:28 2015 +0200
+++ b/src/HOL/HOL.thy	Sat May 09 12:19:24 2015 +0200
@@ -1270,6 +1270,8 @@
 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
 by default simp_all
 
+(* This is not made a simp rule because it does not improve any proofs
+   but slows some AFP entries down by 5% (cpu time). May 2015 *)
 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)
@@ -1297,7 +1299,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
diff -r e1ea5a6379c9 -r 4cd4c204578c src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Thu May 07 15:34:28 2015 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sat May 09 12:19:24 2015 +0200
@@ -169,7 +169,7 @@
 apply oghoare
 --\<open>35 vc\<close>
 apply simp_all
---\<open>21 vc\<close>
+--\<open>16 vc\<close>
 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
 --\<open>11 vc\<close>
 apply simp_all
@@ -433,14 +433,14 @@
 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
 --\<open>112 subgoals left\<close>
 apply(simp_all (no_asm))
---\<open>97 subgoals left\<close>
+--\<open>43 subgoals left\<close>
 apply(tactic \<open>ALLGOALS (conjI_Tac (K all_tac))\<close>)
---\<open>930 subgoals left\<close>
+--\<open>419 subgoals left\<close>
 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
 --\<open>99 subgoals left\<close>
-apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
+apply(simp_all only:length_0_conv [THEN sym])
 --\<open>20 subgoals left\<close>
-apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
+apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
 --\<open>9 subgoals left\<close>
 apply (force simp add:less_Suc_eq)
 apply(hypsubst_thin, drule sym)