src/HOL/Enum.thy
changeset 60429 d3d1e185cd63
parent 60352 d46de31a50c4
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Enum.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Enum.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -817,7 +817,7 @@
     1.4  definition "x - y = x + (- y :: finite_3)"
     1.5  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
     1.6  definition "inverse = (\<lambda>x :: finite_3. x)" 
     1.7 -definition "divide x y = x * inverse (y :: finite_3)"
     1.8 +definition "x div y = x * inverse (y :: finite_3)"
     1.9  definition "abs = (\<lambda>x :: finite_3. x)"
    1.10  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    1.11  definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"