Quelle  LaTeXsugar.thy   Sprache: Isabelle

(*  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  (‹🍋‹\mbox{}\inferrule{\mbox{›_🍋‹}}›🍋‹{\mbox{›_🍋‹}}››)

syntax (Rule output)
  "_bigimpl" :: "asms \ prop \ prop"
  (‹🍋‹\mbox{}\inferrule{›_🍋‹}›🍋‹{\mbox{›_🍋‹}}››)

  "_asms" :: "prop \ asms \ asms" 
  (‹🍋‹\mbox{›_🍋‹}\\›/ _›)

  "_asm" :: "prop \ asms" (‹🍋‹\mbox{›_🍋‹}››)

notation (Axiom output)
  "Trueprop"  (‹🍋‹\mbox{}\inferrule{\mbox{}}{\mbox{›_🍋‹}}››)

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

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

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