Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rule: put \mbox around premises/conclusion to avoid problems with
authorschirmer
Tue, 30 Nov 2004 13:20:15 +0100
changeset 15344 d371b50fcf82
parent 15343 444bb25d3da0
child 15345 3a5c538644ed
Rule: put \mbox around premises/conclusion to avoid problems with super/sub-scripts.
doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle