src/HOL/Enum.thy
changeset 66838 17989f6bc7b2
parent 66817 0b12755ccbb2
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Enum.thy	Mon Oct 09 19:10:48 2017 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Oct 09 19:10:49 2017 +0200
     1.3 @@ -716,7 +716,7 @@
     1.4  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
     1.5  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
     1.6  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
     1.7 -definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
     1.8 +definition [simp]: "division_segment (x :: finite_2) = 1"
     1.9  instance
    1.10    by standard
    1.11      (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
    1.12 @@ -868,7 +868,7 @@
    1.13  definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    1.14  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
    1.15  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
    1.16 -definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
    1.17 +definition [simp]: "division_segment (x :: finite_3) = 1"
    1.18  instance proof
    1.19    fix x :: finite_3
    1.20    assume "x \<noteq> 0"