--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy Thu May 26 17:51:22 2016 +0200
@@ -1,7 +1,7 @@
(* Author: Florian Haftmann, TU Muenchen *)
-section {* Pervasive test of code generator *}
+section \<open>Pervasive test of code generator\<close>
theory Generate_Target_Nat
imports
@@ -11,10 +11,10 @@
"~~/src/HOL/Library/Code_Target_Numeral"
begin
-text {*
+text \<open>
If any of the checks fails, inspect the code generated
- by a corresponding @{text export_code} command.
-*}
+ by a corresponding \<open>export_code\<close> command.
+\<close>
export_code _ checking SML OCaml? Haskell? Scala