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