src/HOL/Library/LaTeXsugar.thy
changeset 60500 903bb1495239
parent 56977 a33fe940a557
child 62522 d32c23d29968
--- a/src/HOL/Library/LaTeXsugar.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -101,7 +101,7 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
-setup{*
+setup\<open>
   let
     fun pretty ctxt c =
       let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
@@ -115,7 +115,7 @@
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
   end;
-*}
+\<close>
 
 end
 (*>*)