src/HOL/Library/Code_Target_Nat.thy
changeset 69593 3dda49e08b9d
parent 68028 1f9f973eed2a
child 69946 494934c30f38
     1.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Code_Abstract_Nat
     1.5  begin
     1.6  
     1.7 -subsection \<open>Implementation for @{typ nat}\<close>
     1.8 +subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close>
     1.9  
    1.10  context
    1.11  includes natural.lifting integer.lifting
    1.12 @@ -163,8 +163,8 @@
    1.13    by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)
    1.14  
    1.15  lemma term_of_nat_code [code]:
    1.16 -  \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
    1.17 -        instead of @{term Code_Target_Nat.Nat} such that reconstructed
    1.18 +  \<comment> \<open>Use \<^term>\<open>Code_Numeral.nat_of_integer\<close> in term reconstruction
    1.19 +        instead of \<^term>\<open>Code_Target_Nat.Nat\<close> such that reconstructed
    1.20          terms can be fed back to the code generator\<close>
    1.21    "term_of_class.term_of n =
    1.22     Code_Evaluation.App