|
(* 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 \<open>
Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
end)
\<close>
end
(*>*)
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
