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/Library/Abstract_Rat.thy
changeset 33657 a4179bf442d1
parent 32960 69916a850301
child 35028 108662d50512 
--- a/src/HOL/Library/Abstract_Rat.thy	Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:14:04 2009 +0100
@@ -206,7 +206,7 @@
       apply simp
       apply algebra
       done
-    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
+    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
       coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
       have eq1: "b = b'" using pos by arith  
       with eq have "a = a'" using pos by simp
isabelle