# HG changeset patch
# User haftmann
# Date 1427571799 -3600
# Node ID d5ccdca16cca1c964eb3cdfc4783c397eaa19c64
# Parent  2333045edb78c786991dc277322d7ba80b9fcd82
dropped long-outdated comments

diff -r 2333045edb78 -r d5ccdca16cca src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Mar 28 21:05:02 2015 +0100
+++ b/src/HOL/Rings.thy	Sat Mar 28 20:43:19 2015 +0100
@@ -197,7 +197,6 @@
 end
 
 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
-  (*previously almost_semiring*)
 begin
 
 subclass semiring_1 ..
@@ -394,7 +393,6 @@
 end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
-  (*previously ring*)
 begin
 
 subclass ring_1 ..
@@ -857,9 +855,6 @@
 
 end
 
-(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
-   Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
- *)
 class linordered_ring_strict = ring + linordered_semiring_strict
   + ordered_ab_group_add + abs_if
 begin
@@ -1006,7 +1001,6 @@
 end
 
 class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
-  (*previously linordered_semiring*)
   assumes zero_less_one [simp]: "0 < 1"
 begin
 
@@ -1040,7 +1034,6 @@
 class linordered_idom = comm_ring_1 +
   linordered_comm_semiring_strict + ordered_ab_group_add +
   abs_if + sgn_if
-  (*previously linordered_ring*)
 begin
 
 subclass linordered_semiring_1_strict ..