src/HOL/Hyperreal/StarClasses.thy
changeset 23551 84f0996a530b
parent 23282 dfc459989d24
child 23879 4776af8be741
equal deleted inserted replaced
23550:d4f1d6ef119c 23551:84f0996a530b
   363 instance star :: (ring) ring ..
   363 instance star :: (ring) ring ..
   364 instance star :: (comm_ring) comm_ring ..
   364 instance star :: (comm_ring) comm_ring ..
   365 instance star :: (ring_1) ring_1 ..
   365 instance star :: (ring_1) ring_1 ..
   366 instance star :: (comm_ring_1) comm_ring_1 ..
   366 instance star :: (comm_ring_1) comm_ring_1 ..
   367 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   367 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   368 instance star :: (dom) dom ..
   368 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
   369 instance star :: (idom) idom .. 
   369 instance star :: (idom) idom .. 
   370 
   370 
   371 instance star :: (division_ring) division_ring
   371 instance star :: (division_ring) division_ring
   372 apply (intro_classes)
   372 apply (intro_classes)
   373 apply (transfer, erule left_inverse)
   373 apply (transfer, erule left_inverse)