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.
modernized notation -- to make it work for authentic syntax;
authorwenzelm
Sun, 21 Feb 2010 20:54:07 +0100
changeset 35251 e244adbbc28f
parent 35250 92664dca6f20
child 35252 24c466b2cdc8
modernized notation -- to make it work for authentic syntax;
src/HOL/Library/LaTeXsugar.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/DFA/Semilat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/LaTeXsugar.thy	Sun Feb 21 20:53:50 2010 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Sun Feb 21 20:54:07 2010 +0100
@@ -64,10 +64,10 @@
 consts DUMMY :: 'a ("\<^raw:\_>")
 
 (* THEOREMS *)
+notation (Rule output)
+  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
 syntax (Rule output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
-
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
 
@@ -76,21 +76,20 @@
 
   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
 
-syntax (Axiom output)
-  "Trueprop" :: "bool \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+notation (Axiom output)
+  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
 
+notation (IfThen output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
 syntax (IfThen output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
 
+notation (IfThenNoBox output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
 syntax (IfThenNoBox output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Feb 21 20:53:50 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Feb 21 20:54:07 2010 +0100
@@ -22,16 +22,17 @@
   "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
   "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" 
 (*<*)
-syntax 
-  "lesub"   :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
-  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
-  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+notation
+  "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
+  "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
+  "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
 (*>*)
-syntax (xsymbols)
-  "lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
-  "lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50)
-  "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
+notation (xsymbols)
+  "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
+  "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
+  "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
 (*<*)
+syntax
  (* allow \<sub> instead of \<bsub>..\<esub> *)  
   "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
   "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
isabelle