src/HOL/Library/LaTeXsugar.thy
changeset 49628 8262d35eff20
parent 41757 7bbd11360bd3
child 55077 4cf280104b85
child 55111 5792f5106c40
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:09:28 2012 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Sep 28 08:39:48 2012 +0200
     1.3 @@ -97,5 +97,21 @@
     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 +  let
     1.9 +    fun pretty ctxt c =
    1.10 +      let val tc = Proof_Context.read_const_proper ctxt false c
    1.11 +      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    1.12 +            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    1.13 +      end
    1.14 +  in
    1.15 +    Thy_Output.antiquotation @{binding "const_typ"}
    1.16 +     (Scan.lift Args.name_source)
    1.17 +       (fn {source = src, context = ctxt, ...} => fn arg =>
    1.18 +          Thy_Output.output ctxt
    1.19 +            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
    1.20 +  end;
    1.21 +*}
    1.22 +
    1.23  end
    1.24  (*>*)
    1.25 \ No newline at end of file