# HG changeset patch
# User schirmer
# Date 1101817776 -3600
# Node ID 3a5c538644ed42bec86b1ea213ca426e5462b7e7
# Parent  d371b50fcf821a7541183660081993be0a8ebe31
even more mboxes

diff -r d371b50fcf82 -r 3a5c538644ed doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy
--- a/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Tue Nov 30 13:20:15 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Tue Nov 30 13:29:36 2004 +0100
@@ -63,7 +63,7 @@
   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
 
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("_\<^raw:\\>/ _")
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
 
   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")