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)"
```