src/HOL/Nonstandard_Analysis/StarDef.thy
changeset 66815 93c6632ddf44
parent 66806 a4e82b58d833
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -834,6 +834,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance star :: (semidom_modulo) semidom_modulo
     1.8 +  by standard (transfer; simp)
     1.9 +
    1.10 +
    1.11  
    1.12  subsection \<open>Power\<close>
    1.13  
    1.14 @@ -917,14 +921,6 @@
    1.15  
    1.16  instance star :: (ring_char_0) ring_char_0 ..
    1.17  
    1.18 -instance star :: (semiring_parity) semiring_parity
    1.19 -  apply intro_classes
    1.20 -     apply (transfer, rule odd_one)
    1.21 -    apply (transfer, erule (1) odd_even_add)
    1.22 -   apply (transfer, erule even_multD)
    1.23 -  apply (transfer, erule odd_ex_decrement)
    1.24 -  done
    1.25 -
    1.26  
    1.27  subsection \<open>Finite class\<close>
    1.28