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/Semiring_Normalization.thy
changeset 37946 be3c0df7bb90
parent 36873 112e613e8d0b
child 47108 2a1953f0d20d 
--- a/src/HOL/Semiring_Normalization.thy	Fri Jul 23 09:05:54 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Fri Jul 23 10:25:00 2010 +0200
@@ -36,7 +36,7 @@
 
 end
 
-sublocale idom < comm_semiring_1_cancel_crossproduct
+subclass (in idom) comm_semiring_1_cancel_crossproduct
 proof
   fix w x y z
   show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
isabelle