--- a/src/HOL/Library/LaTeXsugar.thy Fri Feb 16 09:04:23 2007 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Feb 16 11:00:47 2007 +0100
@@ -79,6 +79,10 @@
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+syntax (Axiom output)
+ "Trueprop" :: "bool \<Rightarrow> prop"
+ ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
syntax (IfThen output)
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")