src/HOL/Library/LaTeXsugar.thy
changeset 22328 cc403d881873
parent 21210 c17fd2df4e9e
child 25467 bba589a88022
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Feb 16 09:04:23 2007 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Feb 16 11:00:47 2007 +0100
     1.3 @@ -79,6 +79,10 @@
     1.4  
     1.5    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
     1.6  
     1.7 +syntax (Axiom output)
     1.8 +  "Trueprop" :: "bool \<Rightarrow> prop"
     1.9 +  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    1.10 +
    1.11  syntax (IfThen output)
    1.12    "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.13    ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")