Quelle  LaTeXsugar.thy

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

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

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