src/HOL/Semiring_Normalization.thy
changeset 37946 be3c0df7bb90
parent 36873 112e613e8d0b
child 47108 2a1953f0d20d
     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"