Theory Prog_Prove.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{}›Iflatex‹\\,}› _/ latex‹{\\normalsize \\,›thenlatex‹\\,}›/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms  prop  prop"
  ("latex‹{\\normalsize{}›Iflatex‹\\,}› _ /latex‹{\\normalsize \\,›thenlatex‹\\,}›/ _.")
  "_asms" :: "prop  asms  asms" ("latex‹\\mbox{›_latex‹}› /latex‹{\\normalsize \\,›andlatex‹\\,}›/ _")
  "_asm" :: "prop  asms" ("latex‹\\mbox{›_latex‹}›")

notation (IfThenNoBox output)
  Pure.imp  ("latex‹{\\normalsize{}›Iflatex‹\\,}› _/ latex‹{\\normalsize \\,›thenlatex‹\\,}›/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms  prop  prop"
  ("latex‹{\\normalsize{}›Iflatex‹\\,}› _ /latex‹{\\normalsize \\,›thenlatex‹\\,}›/ _.")
  "_asms" :: "prop  asms  asms" ("_ /latex‹{\\normalsize \\,›andlatex‹\\,}›/ _")
  "_asm" :: "prop  asms" ("_")

setup Document_Output.antiquotation_pretty_source bindingconst_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
(*>*)