Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorblanchet
Wed, 24 Feb 2010 11:35:39 +0100
changeset 35341 c6bbfa9c4eca
parent 35330 e7eb254db165 (diff)
parent 35340 c32d7269bad1 (current diff)
child 35342 4dc65845eab3
merged
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Feb 24 11:35:10 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Feb 24 11:35:39 2010 +0100
@@ -64,10 +64,8 @@
 subsection {* Euclidean domains *}
 
 (*
-axclass
-  euclidean < "domain"
-
-  euclidean_ax:  "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
+class euclidean = "domain" +
+  assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
                    a = b * q + r & e_size r < e_size b)"
 
   Nothing has been proved about Euclidean domains, yet.
isabelle