# HG changeset patch
# User haftmann
# Date 1267006897 -3600
# Node ID e7eb254db16537efcf0d989db5bb284dad25f606
# Parent  cac5a37fb638c0afbec149b4631746bae893a4e2
tuned comment

diff -r cac5a37fb638 -r e7eb254db165 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Tue Feb 23 17:55:00 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Feb 24 11:21:37 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.