src/Doc/Prog_Prove/LaTeXsugar.thy
changeset 67406 23307fd33906
parent 67399 eab6ce8368fa
child 67463 a5ca98950a91
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -43,7 +43,7 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_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
@@ -57,7 +57,7 @@
           Thy_Output.output ctxt
             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
   end;
-*}
+\<close>
 
 end
 (*>*)