src/HOL/Rings.thy
changeset 61799 4cf66f21b764
parent 61762 d50b993b4fb9
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Rings.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
     1.5  begin
     1.6  
     1.7 -text\<open>For the @{text combine_numerals} simproc\<close>
     1.8 +text\<open>For the \<open>combine_numerals\<close> simproc\<close>
     1.9  lemma combine_common_factor:
    1.10    "a * e + (b * e + c) = (a + b) * e + c"
    1.11  by (simp add: distrib_right ac_simps)
    1.12 @@ -890,7 +890,7 @@
    1.13    by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
    1.14  
    1.15  lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
    1.16 -  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
    1.17 +  dvd_mult_unit_iff dvd_div_unit_iff \<comment> \<open>FIXME consider fact collection\<close>
    1.18  
    1.19  lemma unit_mult_div_div [simp]:
    1.20    "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
    1.21 @@ -1298,7 +1298,7 @@
    1.22  lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
    1.23  using mult_right_mono [of a 0 b] by simp
    1.24  
    1.25 -text \<open>Legacy - use @{text mult_nonpos_nonneg}\<close>
    1.26 +text \<open>Legacy - use \<open>mult_nonpos_nonneg\<close>\<close>
    1.27  lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
    1.28  by (drule mult_right_mono [of b 0], auto)
    1.29  
    1.30 @@ -1374,7 +1374,7 @@
    1.31  lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
    1.32  using mult_strict_right_mono [of a 0 b] by simp
    1.33  
    1.34 -text \<open>Legacy - use @{text mult_neg_pos}\<close>
    1.35 +text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>
    1.36  lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
    1.37  by (drule mult_strict_right_mono [of b 0], auto)
    1.38  
    1.39 @@ -1627,7 +1627,7 @@
    1.40    done
    1.41  
    1.42  text\<open>Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
    1.43 -   also with the relations @{text "\<le>"} and equality.\<close>
    1.44 +   also with the relations \<open>\<le>\<close> and equality.\<close>
    1.45  
    1.46  text\<open>These ``disjunction'' versions produce two cases when the comparison is
    1.47   an assumption, but effectively four when the comparison is a goal.\<close>