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/Computational_Algebra/Euclidean_Algorithm.thy
changeset 67399 eab6ce8368fa
parent 67167 88d1c9d86f48
child 67443 3abf6a722518 
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -422,7 +422,7 @@
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   proof (rule ext)+
@@ -576,7 +576,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   proof (rule ext)+
@@ -613,7 +613,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   proof (rule ext)+
isabelle