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