proper subclass instead of sublocale
authorhaftmann
Fri Jul 23 10:25:00 2010 +0200 (2010-07-23)
changeset 37946be3c0df7bb90
parent 37945 32f9b7a70fc0
child 37947 844977c7abeb
proper subclass instead of sublocale
src/HOL/Semiring_Normalization.thy
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Fri Jul 23 09:05:54 2010 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Fri Jul 23 10:25:00 2010 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -sublocale idom < comm_semiring_1_cancel_crossproduct
     1.8 +subclass (in idom) comm_semiring_1_cancel_crossproduct
     1.9  proof
    1.10    fix w x y z
    1.11    show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"