src/HOL/Enum.thy
changeset 59867 58043346ca64
parent 59582 0fbed69ff081
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/Enum.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Enum.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -683,7 +683,7 @@
     1.4  
     1.5  instance finite_2 :: complete_linorder ..
     1.6  
     1.7 -instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
     1.8 +instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
     1.9  definition [simp]: "0 = a\<^sub>1"
    1.10  definition [simp]: "1 = a\<^sub>2"
    1.11  definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    1.12 @@ -807,7 +807,7 @@
    1.13  
    1.14  instance finite_3 :: complete_linorder ..
    1.15  
    1.16 -instantiation finite_3 :: "{field_inverse_zero, abs_if, ring_div, semiring_div, sgn_if}" begin
    1.17 +instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
    1.18  definition [simp]: "0 = a\<^sub>1"
    1.19  definition [simp]: "1 = a\<^sub>2"
    1.20  definition