src/HOL/Library/LaTeXsugar.thy
changeset 60500 903bb1495239
parent 56977 a33fe940a557
child 62522 d32c23d29968
equal deleted inserted replaced
60499:54a3db2ed201 60500:903bb1495239
    99   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    99   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   100   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   100   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   101   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   101   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   102   "_asm" :: "prop \<Rightarrow> asms" ("_")
   102   "_asm" :: "prop \<Rightarrow> asms" ("_")
   103 
   103 
   104 setup{*
   104 setup\<open>
   105   let
   105   let
   106     fun pretty ctxt c =
   106     fun pretty ctxt c =
   107       let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
   107       let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
   108       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
   108       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
   109             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
   109             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
   113      (Scan.lift Args.name_inner_syntax)
   113      (Scan.lift Args.name_inner_syntax)
   114        (fn {source = src, context = ctxt, ...} => fn arg =>
   114        (fn {source = src, context = ctxt, ...} => fn arg =>
   115           Thy_Output.output ctxt
   115           Thy_Output.output ctxt
   116             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
   116             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
   117   end;
   117   end;
   118 *}
   118 \<close>
   119 
   119 
   120 end
   120 end
   121 (*>*)
   121 (*>*)