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