# 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 \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") + ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") "_asms" :: "prop \ asms \ asms" ("_\<^raw:\\>/ _") - "_asm" :: "prop \ asms" ("_") + "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") syntax (IfThen output) "==>" :: "prop \ prop \ prop"