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.
proper subclass instead of sublocale
authorhaftmann
Fri, 23 Jul 2010 10:25:00 +0200
changeset 37946 be3c0df7bb90
parent 37945 32f9b7a70fc0
child 37947 844977c7abeb
proper subclass instead of sublocale
src/HOL/Semiring_Normalization.thy file | annotate | diff | comparison | revisions 
--- 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