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{}›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
(*>*)