Theory Prog_Prove.LaTeXsugar
theory LaTeXsugar
imports Main
begin
consts DUMMY :: 'a ("\<^latex>‹\\_›")
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