# HG changeset patch
# User blanchet
# Date 1267007739 -3600
# Node ID c6bbfa9c4eca6b17f2b4f69be5bbca25a7585eda
# Parent  e7eb254db16537efcf0d989db5bb284dad25f606# Parent  c32d7269bad19925cd9b5a051ba6f94c722ad61b
merged

diff -r c32d7269bad1 -r c6bbfa9c4eca src/HOL/Algebra/abstract/Ring2.thy
--- 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.