src/HOL/Int.thy
changeset 61799 4cf66f21b764
parent 61738 c4f6031f1310
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Int.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -198,7 +198,7 @@
     1.4    for z1 z2 w :: int
     1.5  
     1.6  
     1.7 -subsection \<open>Embedding of the Integers into any @{text ring_1}: @{text of_int}\<close>
     1.8 +subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
     1.9  
    1.10  context ring_1
    1.11  begin
    1.12 @@ -270,7 +270,7 @@
    1.13  context linordered_idom
    1.14  begin
    1.15  
    1.16 -text\<open>Every @{text linordered_idom} has characteristic zero.\<close>
    1.17 +text\<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
    1.18  subclass ring_char_0 ..
    1.19  
    1.20  lemma of_int_le_iff [simp]:
    1.21 @@ -364,7 +364,7 @@
    1.22    apply simp
    1.23    done
    1.24  
    1.25 -subsection \<open>Magnitude of an Integer, as a Natural Number: @{text nat}\<close>
    1.26 +subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
    1.27  
    1.28  lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
    1.29    by auto
    1.30 @@ -525,9 +525,9 @@
    1.31  by simp
    1.32  
    1.33  text\<open>This version is proved for all ordered rings, not just integers!
    1.34 -      It is proved here because attribute @{text arith_split} is not available
    1.35 -      in theory @{text Rings}.
    1.36 -      But is it really better than just rewriting with @{text abs_if}?\<close>
    1.37 +      It is proved here because attribute \<open>arith_split\<close> is not available
    1.38 +      in theory \<open>Rings\<close>.
    1.39 +      But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
    1.40  lemma abs_split [arith_split, no_atp]:
    1.41       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
    1.42  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    1.43 @@ -588,14 +588,14 @@
    1.44    using assms by (rule nonneg_eq_int)
    1.45  
    1.46  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    1.47 -  -- \<open>Unfold all @{text let}s involving constants\<close>
    1.48 -  by (fact Let_numeral) -- \<open>FIXME drop\<close>
    1.49 +  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    1.50 +  by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
    1.51  
    1.52  lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
    1.53 -  -- \<open>Unfold all @{text let}s involving constants\<close>
    1.54 -  by (fact Let_neg_numeral) -- \<open>FIXME drop\<close>
    1.55 +  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    1.56 +  by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
    1.57  
    1.58 -text \<open>Unfold @{text min} and @{text max} on numerals.\<close>
    1.59 +text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
    1.60  
    1.61  lemmas max_number_of [simp] =
    1.62    max_def [of "numeral u" "numeral v"]
    1.63 @@ -1220,7 +1220,7 @@
    1.64  lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
    1.65  
    1.66  
    1.67 -text \<open>Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
    1.68 +text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
    1.69    strange, but then other simprocs simplify the quotient.\<close>
    1.70  
    1.71  lemmas inverse_eq_divide_numeral [simp] =
    1.72 @@ -1250,10 +1250,10 @@
    1.73  lemmas minus_less_iff_numeral [no_atp] =
    1.74    minus_less_iff [of _ "numeral v"] for v
    1.75  
    1.76 --- \<open>FIXME maybe simproc\<close>
    1.77 +\<comment> \<open>FIXME maybe simproc\<close>
    1.78  
    1.79  
    1.80 -text \<open>Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"})\<close>
    1.81 +text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
    1.82  
    1.83  lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
    1.84  lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
    1.85 @@ -1261,7 +1261,7 @@
    1.86  lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
    1.87  
    1.88  
    1.89 -text \<open>Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="})\<close>
    1.90 +text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
    1.91  
    1.92  named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
    1.93  
    1.94 @@ -1689,7 +1689,7 @@
    1.95  lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    1.96  lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    1.97  
    1.98 -text \<open>De-register @{text "int"} as a quotient type:\<close>
    1.99 +text \<open>De-register \<open>int\<close> as a quotient type:\<close>
   1.100  
   1.101  lifting_update int.lifting
   1.102  lifting_forget int.lifting