src/HOL/Enum.thy
changeset 58710 7216a10d69ba
parent 58659 6c9821c32dd5
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Enum.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -705,10 +705,6 @@
     1.4    "2 = a\<^sub>1"
     1.5    by (simp add: numeral.simps plus_finite_2_def)
     1.6    
     1.7 -instance finite_2 :: semiring_div_parity
     1.8 -by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
     1.9 -
    1.10 -
    1.11  hide_const (open) a\<^sub>1 a\<^sub>2
    1.12  
    1.13  datatype (plugins only: code "quickcheck" extraction) finite_3 =