src/HOL/Rings.thy
changeset 59832 d5ccdca16cca
parent 59816 034b13f4efae
child 59833 ab828c2c5d67
     1.1 --- a/src/HOL/Rings.thy	Sat Mar 28 21:05:02 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Sat Mar 28 20:43:19 2015 +0100
     1.3 @@ -197,7 +197,6 @@
     1.4  end
     1.5  
     1.6  class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
     1.7 -  (*previously almost_semiring*)
     1.8  begin
     1.9  
    1.10  subclass semiring_1 ..
    1.11 @@ -394,7 +393,6 @@
    1.12  end
    1.13  
    1.14  class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
    1.15 -  (*previously ring*)
    1.16  begin
    1.17  
    1.18  subclass ring_1 ..
    1.19 @@ -857,9 +855,6 @@
    1.20  
    1.21  end
    1.22  
    1.23 -(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
    1.24 -   Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
    1.25 - *)
    1.26  class linordered_ring_strict = ring + linordered_semiring_strict
    1.27    + ordered_ab_group_add + abs_if
    1.28  begin
    1.29 @@ -1006,7 +1001,6 @@
    1.30  end
    1.31  
    1.32  class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
    1.33 -  (*previously linordered_semiring*)
    1.34    assumes zero_less_one [simp]: "0 < 1"
    1.35  begin
    1.36  
    1.37 @@ -1040,7 +1034,6 @@
    1.38  class linordered_idom = comm_ring_1 +
    1.39    linordered_comm_semiring_strict + ordered_ab_group_add +
    1.40    abs_if + sgn_if
    1.41 -  (*previously linordered_ring*)
    1.42  begin
    1.43  
    1.44  subclass linordered_semiring_1_strict ..