src/HOL/Computational_Algebra/Field_as_Ring.thy
 changeset 66838 17989f6bc7b2 parent 66817 0b12755ccbb2
```     1.1 --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:48 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Mon Oct 09 19:10:49 2017 +0200
1.3 @@ -29,9 +29,9 @@
1.4
1.5  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
1.6  definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
1.7 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
1.8  definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
1.9 -definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
1.10 -definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
1.11 +definition [simp]: "division_segment (x :: real) = 1"
1.12
1.13  instance
1.14    by standard
1.15 @@ -60,9 +60,9 @@
1.16
1.17  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
1.18  definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
1.19 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
1.20  definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
1.21 -definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
1.22 -definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
1.23 +definition [simp]: "division_segment (x :: rat) = 1"
1.24
1.25  instance
1.26    by standard
1.27 @@ -91,9 +91,9 @@
1.28
1.29  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
1.30  definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
1.31 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
1.32  definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
1.33 -definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
1.34 -definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
1.35 +definition [simp]: "division_segment (x :: complex) = 1"
1.36
1.37  instance
1.38    by standard
```