equal
deleted
inserted
replaced
98 "_asm" :: "prop \<Rightarrow> asms" ("_") |
98 "_asm" :: "prop \<Rightarrow> asms" ("_") |
99 |
99 |
100 setup{* |
100 setup{* |
101 let |
101 let |
102 fun pretty ctxt c = |
102 fun pretty ctxt c = |
103 let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c |
103 let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c |
104 in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", |
104 in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", |
105 Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] |
105 Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] |
106 end |
106 end |
107 in |
107 in |
108 Thy_Output.antiquotation @{binding "const_typ"} |
108 Thy_Output.antiquotation @{binding "const_typ"} |