# HG changeset patch # User haftmann # Date 1279873500 -7200 # Node ID be3c0df7bb90cc67398b61af1a70b842c923bd16 # Parent 32f9b7a70fc0d1df83e1eb42ff314958b2f94f55 proper subclass instead of sublocale diff -r 32f9b7a70fc0 -r be3c0df7bb90 src/HOL/Semiring_Normalization.thy --- 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 \ w = x \ y = z"