# HG changeset patch # User nipkow # Date 1196097906 -3600 # Node ID bba589a880220020d25d0449c527685304d8b9f1 # Parent 3f72994ec0969d330700e24cc6c6b6cffca1d709 Removed forced roman font in mode=IfThen. diff -r 3f72994ec096 -r bba589a88022 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Mon Nov 26 18:01:48 2007 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Mon Nov 26 18:25:06 2007 +0100 @@ -85,18 +85,18 @@ syntax (IfThen output) "==>" :: "prop \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") syntax (IfThenNoBox output) "==>" :: "prop \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") "_asm" :: "prop \ asms" ("_") end