src/HOL/Library/Code_Target_Int.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60868 dd18c33c001e
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Implementation of integer numbers by target-language integers *}
     1.8 +section \<open>Implementation of integer numbers by target-language integers\<close>
     1.9  
    1.10  theory Code_Target_Int
    1.11  imports Main