| changeset 45542 | 4849dbe6e310 |
| parent 40815 | 6e2d17cc0d1d |
| child 45605 | a89b4bc311a5 |
--- a/src/HOL/NSA/StarDef.thy Thu Nov 17 07:55:09 2011 +0100 +++ b/src/HOL/NSA/StarDef.thy Thu Nov 17 08:07:54 2011 +0100 @@ -1008,6 +1008,9 @@ instance star :: (ring_char_0) ring_char_0 .. +instance star :: (number_semiring) number_semiring +by (intro_classes, simp only: star_number_def star_of_nat_def number_of_int) + instance star :: (number_ring) number_ring by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)