src/HOL/Library/LaTeXsugar.thy
changeset 25467 bba589a88022
parent 22328 cc403d881873
child 25595 6c48275f9c76
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Mon Nov 26 18:01:48 2007 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Nov 26 18:25:06 2007 +0100
     1.3 @@ -85,18 +85,18 @@
     1.4  
     1.5  syntax (IfThen output)
     1.6    "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
     1.7 -  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
     1.8 +  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
     1.9    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.10 -  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.11 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.12 +  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.13 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    1.14    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.15  
    1.16  syntax (IfThenNoBox output)
    1.17    "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.18 -  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.19 +  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.20    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.21 -  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
    1.22 -  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
    1.23 +  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.24 +  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    1.25    "_asm" :: "prop \<Rightarrow> asms" ("_")
    1.26  
    1.27  end