src/HOL/Library/LaTeXsugar.thy
changeset 35251 e244adbbc28f
parent 31462 4fcbf17b5a98
child 41757 7bbd11360bd3
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun Feb 21 20:53:50 2010 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Sun Feb 21 20:54:07 2010 +0100
     1.3 @@ -64,10 +64,10 @@
     1.4  consts DUMMY :: 'a ("\<^raw:\_>")
     1.5  
     1.6  (* THEOREMS *)
     1.7 +notation (Rule output)
     1.8 +  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
     1.9 +
    1.10  syntax (Rule output)
    1.11 -  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.12 -  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.13 -
    1.14    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.15    ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
    1.16  
    1.17 @@ -76,21 +76,20 @@
    1.18  
    1.19    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.20  
    1.21 -syntax (Axiom output)
    1.22 -  "Trueprop" :: "bool \<Rightarrow> prop"
    1.23 -  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    1.24 +notation (Axiom output)
    1.25 +  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
    1.26  
    1.27 +notation (IfThen output)
    1.28 +  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.29  syntax (IfThen output)
    1.30 -  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.31 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.32    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.33    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.34    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
    1.35    "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
    1.36  
    1.37 +notation (IfThenNoBox output)
    1.38 +  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.39  syntax (IfThenNoBox output)
    1.40 -  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
    1.41 -  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.42    "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
    1.43    ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
    1.44    "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")