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 (‹🚫‹\_››)

(* 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
(*>*)