modernized notation -- to make it work for authentic syntax;
authorwenzelm
Sun Feb 21 20:54:07 2010 +0100 (2010-02-21)
changeset 35251e244adbbc28f
parent 35250 92664dca6f20
child 35252 24c466b2cdc8
modernized notation -- to make it work for authentic syntax;
src/HOL/Library/LaTeXsugar.thy
src/HOL/MicroJava/DFA/Semilat.thy
     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:\,}>/ _")
     2.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Feb 21 20:53:50 2010 +0100
     2.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Feb 21 20:54:07 2010 +0100
     2.3 @@ -22,16 +22,17 @@
     2.4    "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
     2.5    "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
     2.6  (*<*)
     2.7 -syntax 
     2.8 -  "lesub"   :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
     2.9 -  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
    2.10 -  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
    2.11 +notation
    2.12 +  "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
    2.13 +  "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
    2.14 +  "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
    2.15  (*>*)
    2.16 -syntax (xsymbols)
    2.17 -  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
    2.18 -  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
    2.19 -  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
    2.20 +notation (xsymbols)
    2.21 +  "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    2.22 +  "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    2.23 +  "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
    2.24  (*<*)
    2.25 +syntax
    2.26   (* allow \<sub> instead of \<bsub>..\<esub> *)  
    2.27    "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    2.28    "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)