# HG changeset patch
# User schirmer
# Date 1101817215 -3600
# Node ID d371b50fcf821a7541183660081993be0a8ebe31
# Parent  444bb25d3da0f22a4581e4f614475602b83ced24
Rule: put \mbox around premises/conclusion to avoid problems with
super/sub-scripts.

diff -r 444bb25d3da0 -r d371b50fcf82 doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy
--- a/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Tue Nov 30 06:50:03 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Tue Nov 30 13:20:15 2004 +0100
@@ -57,15 +57,15 @@
 (* THEOREMS *)
 syntax (Rule output)
   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
 
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
 
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
   ("_\<^raw:\\>/ _")
 
-  "_asm" :: "prop \<Rightarrow> asms" ("_")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
 
 syntax (IfThen output)
   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"