src/HOL/Real/PReal.thy

     show "\<exists>y'\<in>B. z = (z/y) * y'"
     proof
       show "z = (z/y)*y"
 	by (simp add: divide_inverse mult_commute [of y] mult_assoc
 		      order_less_imp_not_eq2)
-      show "y \<in> B" .
+      show "y \<in> B" by fact
     qed
   next
     show "z/y \<in> A"
     proof (rule preal_downwards_closed [OF A x])
       show "0 < z/y"

         show "\<exists>v'\<in>A. x = (x / v) * v'"
         proof
           show "x = (x/v)*v"
 	    by (simp add: divide_inverse mult_assoc vpos
                           order_less_imp_not_eq2)
-          show "v \<in> A" .
+          show "v \<in> A" by fact
         qed
       qed
     qed
   qed
   thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"

   hence zpos:  "0 < z" using prems by (simp add: zero_less_mult_iff)
   have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
     by (simp add: mult_ac)
   also have "... = x/y" using zpos
     by (simp add: divide_inverse)
-  also have "... < z"
-    by (simp add: pos_divide_less_eq [OF ypos] mult_commute) 
+  also from xless have "... < z"
+    by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
   finally show ?thesis .
 qed
 
 lemma preal_of_rat_mult_lemma3:
   assumes uless: "u < x * y"