src/HOL/Nat.thy

 text {* Associative law for multiplication *}
 lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   by (induct m) (simp_all add: add_mult_distrib)
 
 
-text{*The Naturals Form A comm_semiring_1_cancel*}
+text{*The naturals form a @{text comm_semiring_1_cancel}*}
 instance nat :: comm_semiring_1_cancel
 proof
   fix i j k :: nat
   show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   show "i + j = j + i" by (rule nat_add_commute)

   apply (induct_tac x) 
   apply (simp_all add: add_less_mono)
   done
 
 
-text{*The Naturals Form an Ordered comm_semiring_1_cancel*}
+text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
 instance nat :: ordered_semidom
 proof
   fix i j k :: nat
   show "0 < (1::nat)" by simp
   show "i \<le> j ==> k + i \<le> k + j" by simp