diff -r 10d0fb526643 -r ded2364d14d4 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 08:26:08 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 09:03:24 2009 -0700
@@ -102,25 +102,21 @@
 instance proof
   fix x y :: "'a \<times> 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
-    unfolding dist_prod_def
-    by (simp add: expand_prod_eq)
+    unfolding dist_prod_def expand_prod_eq by simp
 next
   fix x y z :: "'a \<times> 'b"
   show "dist x y \<le> dist x z + dist y z"
     unfolding dist_prod_def
-    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
-    apply (rule real_sqrt_le_mono)
-    apply (rule order_trans [OF add_mono])
-    apply (rule power_mono [OF dist_triangle2 [of _ _ "fst z"] zero_le_dist])
-    apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
-    apply (simp only: real_sum_squared_expand)
-    done
+    by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]
+        real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
 next
   (* FIXME: long proof! *)
   (* Maybe it would be easier to define topological spaces *)
   (* in terms of neighborhoods instead of open sets? *)
   fix S :: "('a \<times> 'b) set"
   show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  proof
+    assume "open S" thus "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
     unfolding open_prod_def open_dist
     apply safe
     apply (drule (1) bspec)
@@ -136,7 +132,11 @@
     apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
     apply (drule spec, erule mp)
     apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
-
+    done
+  next
+    assume "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" thus "open S"
+    unfolding open_prod_def open_dist
+    apply safe
     apply (drule (1) bspec)
     apply clarify
     apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
@@ -147,14 +147,14 @@
     apply clarify
     apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
     apply clarify
-    apply (rule le_less_trans [OF dist_triangle])
-    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (simp add: less_diff_eq)
+    apply (erule le_less_trans [OF dist_triangle])
     apply (rule conjI)
     apply clarify
     apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
     apply clarify
-    apply (rule le_less_trans [OF dist_triangle])
-    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (simp add: less_diff_eq)
+    apply (erule le_less_trans [OF dist_triangle])
     apply (rule conjI)
     apply simp
     apply (clarify, rename_tac c d)
@@ -164,6 +164,7 @@
     apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
     apply (simp add: power_divide)
     done
+  qed
 qed
 
 end