author | nipkow |
Mon, 11 Jun 2007 16:21:03 +0200 | |
changeset 23326 | 71e99443e17d |
parent 23325 | 156db04f8af0 |
child 23327 | 1654013ec97c |
--- a/src/HOL/Ring_and_Field.thy Mon Jun 11 11:10:04 2007 +0200 +++ b/src/HOL/Ring_and_Field.thy Mon Jun 11 16:21:03 2007 +0200 @@ -125,6 +125,7 @@ class ring_no_zero_divisors = ring + no_zero_divisors class dom = ring_1 + ring_no_zero_divisors +hide const dom class idom = comm_ring_1 + no_zero_divisors