Theory LaTeXsugar

(*  Title:      HOL/Library/LaTeXsugar.thy
    Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
    Copyright   2005 NICTA and TUM
*)

(*<*)
theory LaTeXsugar
imports Main
begin

(* DUMMY *)
consts DUMMY :: 'a ("\<^latex>‹\\_›")

(* THEOREMS *)
notation (Rule output)
  Pure.imp  ("\<^latex>‹\\mbox{}\\inferrule{\\mbox{›_\<^latex>‹}}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

syntax (Rule output)
  "_bigimpl" :: "asms ⇒ prop ⇒ prop"
  ("\<^latex>‹\\mbox{}\\inferrule{›_\<^latex>‹}›\<^latex>‹{\\mbox{›_\<^latex>‹}}›")

  "_asms" :: "prop ⇒ asms ⇒ asms" 
  ("\<^latex>‹\\mbox{›_\<^latex>‹}\\\\›/ _")

  "_asm" :: "prop ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}›")

notation (Axiom output)
  "Trueprop"  ("\<^latex>‹\\mbox{}\\inferrule{\\mbox{}}{\\mbox{›_\<^latex>‹}}›")

notation (IfThen output)
  Pure.imp  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _/ \<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms ⇒ prop ⇒ prop"
  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _ /\<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
  "_asms" :: "prop ⇒ asms ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}› /\<^latex>‹{\\normalsize \\,›and\<^latex>‹\\,}›/ _")
  "_asm" :: "prop ⇒ asms" ("\<^latex>‹\\mbox{›_\<^latex>‹}›")

notation (IfThenNoBox output)
  Pure.imp  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _/ \<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms ⇒ prop ⇒ prop"
  ("\<^latex>‹{\\normalsize{}›If\<^latex>‹\\,}› _ /\<^latex>‹{\\normalsize \\,›then\<^latex>‹\\,}›/ _.")
  "_asms" :: "prop ⇒ asms ⇒ asms" ("_ /\<^latex>‹{\\normalsize \\,›and\<^latex>‹\\,}›/ _")
  "_asm" :: "prop ⇒ asms" ("_")

setup ‹
  Document_Output.antiquotation_pretty_source \<^binding>‹const_typ›
    (Scan.lift Parse.embedded_inner_syntax)
    (fn ctxt => fn c =>
      let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
        Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
      end)
›

end
(*>*)