src/HOL/NSA/StarDef.thy
changeset 59833 ab828c2c5d67
parent 59816 034b13f4efae
child 59867 58043346ca64
     1.1 --- a/src/HOL/NSA/StarDef.thy	Sat Mar 28 20:43:19 2015 +0100
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Sat Mar 28 21:32:48 2015 +0100
     1.3 @@ -853,7 +853,7 @@
     1.4  instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
     1.5  by intro_classes (transfer, fact right_diff_distrib')
     1.6  
     1.7 -instance star :: (no_zero_divisors) no_zero_divisors
     1.8 +instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
     1.9  by (intro_classes, transfer, rule no_zero_divisors)
    1.10  
    1.11  instance star :: (semiring_1_cancel) semiring_1_cancel ..
    1.12 @@ -862,7 +862,7 @@
    1.13  instance star :: (comm_ring) comm_ring ..
    1.14  instance star :: (ring_1) ring_1 ..
    1.15  instance star :: (comm_ring_1) comm_ring_1 ..
    1.16 -instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors ..
    1.17 +instance star :: (semidom) semidom ..
    1.18  instance star :: (semiring_div) semiring_div
    1.19  apply intro_classes
    1.20  apply(transfer, rule mod_div_equality)