# HG changeset patch
# User wenzelm
# Date 1340638880 -7200
# Node ID 602dc021595461af305ce4914e7ae04243a282b5
# Parent  87c831e30f0ab99c4dab3f1a3dfc69457a94aaea
tuned proofs -- prefer direct "rotated" instead of old-style COMP;

diff -r 87c831e30f0a -r 602dc0215954 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 25 15:14:07 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 17:41:20 2012 +0200
@@ -865,7 +865,7 @@
     case (insert x F) then show ?case apply -
     apply (simp add: subset_insert_iff, clarify)
     apply (subgoal_tac "finite C")
-      prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+      prefer 2 apply (blast dest: finite_subset [rotated])
     apply (subgoal_tac "C = insert x (C - {x})")
       prefer 2 apply blast
     apply (erule ssubst)
@@ -1517,7 +1517,7 @@
   apply - apply (erule finite_induct) apply simp
   apply (simp add: subset_insert_iff, clarify)
   apply (subgoal_tac "finite C")
-  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+  prefer 2 apply (blast dest: finite_subset [rotated])
   apply (subgoal_tac "C = insert x (C - {x})")
   prefer 2 apply blast
   apply (erule ssubst)
diff -r 87c831e30f0a -r 602dc0215954 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 15:14:07 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 17:41:20 2012 +0200
@@ -511,7 +511,7 @@
   hence "path_component (S i) x z" and "path_component (S j) z y"
     using assms by (simp_all add: path_connected_component)
   hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
-    using *(1,3) by (auto elim!: path_component_of_subset [COMP swap_prems_rl])
+    using *(1,3) by (auto elim!: path_component_of_subset [rotated])
   thus "path_component (\<Union>i\<in>A. S i) x y"
     by (rule path_component_trans)
 qed
diff -r 87c831e30f0a -r 602dc0215954 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 15:14:07 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 17:41:20 2012 +0200
@@ -4208,7 +4208,7 @@
 apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
 apply (rule_tac x="r1 \<circ> r2" in exI)
 apply (rule conjI, simp add: subseq_def)
-apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption)
+apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
 apply (drule (1) tendsto_Pair) back
 apply (simp add: o_def)
 done