src/HOL/Numeral_Simprocs.thy
changeset 61799 4cf66f21b764
parent 60758 d8d85a8172b5
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -23,12 +23,12 @@
     1.4  declare split_div [of _ _ "numeral k", arith_split] for k
     1.5  declare split_mod [of _ _ "numeral k", arith_split] for k
     1.6  
     1.7 -text \<open>For @{text combine_numerals}\<close>
     1.8 +text \<open>For \<open>combine_numerals\<close>\<close>
     1.9  
    1.10  lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
    1.11  by (simp add: add_mult_distrib)
    1.12  
    1.13 -text \<open>For @{text cancel_numerals}\<close>
    1.14 +text \<open>For \<open>cancel_numerals\<close>\<close>
    1.15  
    1.16  lemma nat_diff_add_eq1:
    1.17       "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
    1.18 @@ -62,7 +62,7 @@
    1.19       "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
    1.20  by (auto split add: nat_diff_split simp add: add_mult_distrib)
    1.21  
    1.22 -text \<open>For @{text cancel_numeral_factors}\<close>
    1.23 +text \<open>For \<open>cancel_numeral_factors\<close>\<close>
    1.24  
    1.25  lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
    1.26  by auto
    1.27 @@ -83,7 +83,7 @@
    1.28  lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
    1.29  by(auto)
    1.30  
    1.31 -text \<open>For @{text cancel_factor}\<close>
    1.32 +text \<open>For \<open>cancel_factor\<close>\<close>
    1.33  
    1.34  lemmas nat_mult_le_cancel_disj = mult_le_cancel1
    1.35