src/HOL/Library/LaTeXsugar.thy
changeset 49628 8262d35eff20
parent 41757 7bbd11360bd3
child 55077 4cf280104b85
child 55111 5792f5106c40
equal deleted inserted replaced
49627:34ada66545ca 49628:8262d35eff20
    95   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    95   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    96   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    96   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    97   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    97   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    98   "_asm" :: "prop \<Rightarrow> asms" ("_")
    98   "_asm" :: "prop \<Rightarrow> asms" ("_")
    99 
    99 
       
   100 setup{*
       
   101   let
       
   102     fun pretty ctxt c =
       
   103       let val tc = Proof_Context.read_const_proper ctxt false c
       
   104       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
       
   105             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       
   106       end
       
   107   in
       
   108     Thy_Output.antiquotation @{binding "const_typ"}
       
   109      (Scan.lift Args.name_source)
       
   110        (fn {source = src, context = ctxt, ...} => fn arg =>
       
   111           Thy_Output.output ctxt
       
   112             (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
       
   113   end;
       
   114 *}
       
   115 
   100 end
   116 end
   101 (*>*)
   117 (*>*)