--- a/src/HOL/Enum.thy Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Enum.thy Fri Jun 12 08:53:23 2015 +0200
@@ -817,7 +817,7 @@
definition "x - y = x + (- y :: finite_3)"
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)"
definition "inverse = (\<lambda>x :: finite_3. x)"
-definition "divide x y = x * inverse (y :: finite_3)"
+definition "x div y = x * inverse (y :: finite_3)"
definition "abs = (\<lambda>x :: finite_3. x)"
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)"
definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"