src/HOL/Library/Polynomial_Factorial.thy
changeset 63950 cdc1e59aa513
parent 63905 1c3dcb5fe6cb
child 63954 fb03766658f4
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
     1.5  definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
     1.6  definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
     1.7 -definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
     1.8 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
     1.9  
    1.10  instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.11  end
    1.12 @@ -94,7 +94,7 @@
    1.13  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    1.14  definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    1.15  definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    1.16 -definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
    1.17 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    1.18  
    1.19  instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.20  end
    1.21 @@ -121,7 +121,7 @@
    1.22  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
    1.23  definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
    1.24  definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
    1.25 -definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
    1.26 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
    1.27  
    1.28  instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.29  end