hid constant "dom"
authornipkow
Mon, 11 Jun 2007 16:21:03 +0200
changeset 23326 71e99443e17d
parent 23325 156db04f8af0
child 23327 1654013ec97c
hid constant "dom"
src/HOL/Ring_and_Field.thy
--- 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