--- a/src/HOL/Library/Code_Target_Nat.thy Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Wed Jun 17 11:03:05 2015 +0200
@@ -2,13 +2,13 @@
Author: Florian Haftmann, TU Muenchen
*)
-section {* Implementation of natural numbers by target-language integers *}
+section \<open>Implementation of natural numbers by target-language integers\<close>
theory Code_Target_Nat
imports Code_Abstract_Nat
begin
-subsection {* Implementation for @{typ nat} *}
+subsection \<open>Implementation for @{typ nat}\<close>
context
includes natural.lifting integer.lifting
@@ -129,9 +129,9 @@
including integer.lifting by transfer auto
lemma term_of_nat_code [code]:
- -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
+ -- \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
instead of @{term Code_Target_Nat.Nat} such that reconstructed
- terms can be fed back to the code generator *}
+ terms can be fed back to the code generator\<close>
"term_of_class.term_of n =
Code_Evaluation.App
(Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')