Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
authorwenzelm
Tue, 03 Jul 2007 20:26:08 +0200
changeset 23551 84f0996a530b
parent 23550 d4f1d6ef119c
child 23552 6403d06abe25
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 18:42:09 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 20:26:08 2007 +0200
@@ -365,7 +365,7 @@
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
-instance star :: (dom) dom ..
+instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom .. 
 
 instance star :: (division_ring) division_ring
isabelle