src/HOL/Library/Code_Target_Numeral.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60868 dd18c33c001e
--- a/src/HOL/Library/Code_Target_Numeral.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Code_Target_Numeral.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-section {* Implementation of natural and integer numbers by target-language integers *}
+section \<open>Implementation of natural and integer numbers by target-language integers\<close>
 
 theory Code_Target_Numeral
 imports Code_Target_Int Code_Target_Nat