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
```