hid constant "dom"
authornipkow
Mon Jun 11 16:21:03 2007 +0200 (2007-06-11)
changeset 2332671e99443e17d
parent 23325 156db04f8af0
child 23327 1654013ec97c
hid constant "dom"
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Jun 11 11:10:04 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Jun 11 16:21:03 2007 +0200
     1.3 @@ -125,6 +125,7 @@
     1.4  class ring_no_zero_divisors = ring + no_zero_divisors
     1.5  
     1.6  class dom = ring_1 + ring_no_zero_divisors
     1.7 +hide const dom
     1.8  
     1.9  class idom = comm_ring_1 + no_zero_divisors
    1.10