diff -r 4bee4828cfc3 -r 7ddf297cfcde src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jul 20 09:05:34 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jul 21 13:30:43 2018 +0200
@@ -512,13 +512,11 @@
 
 lemma scaleR_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b"
   for a b :: "'a::ordered_real_vector"
-  apply (drule scaleR_left_mono [of _ _ "- c"], simp_all)
-  done
+  by (drule scaleR_left_mono [of _ _ "- c"], simp_all)
 
 lemma scaleR_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R c"
   for c :: "'a::ordered_real_vector"
-  apply (drule scaleR_right_mono [of _ _ "- c"], simp_all)
-  done
+  by (drule scaleR_right_mono [of _ _ "- c"], simp_all)
 
 lemma scaleR_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>R b"
   for b :: "'a::ordered_real_vector"
@@ -1433,10 +1431,7 @@
 
 lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
   apply standard
-      apply (rule add_right)
-     apply (rule add_left)
-    apply (rule scaleR_right)
-   apply (rule scaleR_left)
+      apply (simp_all add: add_right add_left scaleR_right scaleR_left)
   by (metis bounded mult.commute)
 
 lemma comp1:
@@ -1496,11 +1491,7 @@
 proof -
   interpret f: bounded_linear f by fact
   show ?thesis
-    apply unfold_locales
-      apply (simp add: f.add)
-     apply (simp add: f.scaleR)
-    apply (simp add: f.bounded)
-    done
+    by unfold_locales (simp_all add: f.add f.scaleR f.bounded)
 qed
 
 lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"