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.
add classes ring_no_zero_divisors and dom
authorhuffman
Thu, 17 May 2007 19:29:39 +0200
changeset 22992 fc54d5fc4a7a
parent 22991 b9e2a133e84e
child 22993 838c66e760b5
add classes ring_no_zero_divisors and dom
src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:12:47 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu May 17 19:29:39 2007 +0200
@@ -364,6 +364,8 @@
 instance star :: (comm_ring) comm_ring ..
 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 :: (idom) idom .. 
 
 instance star :: (division_ring) division_ring
isabelle