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.
tuned comment
authorhaftmann
Wed, 24 Feb 2010 11:21:37 +0100
changeset 35330 e7eb254db165
parent 35329 cac5a37fb638
child 35341 c6bbfa9c4eca
child 35366 6d474096698c
tuned comment
src/HOL/Algebra/abstract/Ring2.thy file | annotate | diff | comparison | revisions 
--- 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.
isabelle