Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Complex/ex/Sqrt.thy
changeset 23413 5caa2710dd5b
parent 21404 eb85850d3eb7
child 27556 292098f2efdf 
--- a/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -44,8 +44,7 @@
   have "\<bar>x\<bar> = real ?k / real ?l"
   proof -
     from gcd have "real ?k / real ?l =
-        real (?gcd * ?k) / real (?gcd * ?l)"
-      by (simp add: mult_divide_cancel_left)
+        real (?gcd * ?k) / real (?gcd * ?l)" by simp
     also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
     also from x_rat have "\<dots> = \<bar>x\<bar>" ..
     finally show ?thesis ..
isabelle