src/HOL/Library/OptionalSugar.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/OptionalSugar.thy	Wed Jan 26 13:50:59 2005 +0100
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Library/OptionalSugar.thy
+    ID:         $Id$
+    Author:     Gerwin Klain, Tobias Nipkow
+    Copyright   2005 NICTA and TUM
+*)
+
+theory OptionalSugar
+imports LaTeXsugar
+begin
+
+(* append *)
+syntax (latex output)
+  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+translations
+  "appendL xs ys" <= "xs @ ys" 
+  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+
+
+(* aligning equations *)
+syntax (tab output)
+  "op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
+  "==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+
+(* Let *)
+translations 
+  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
+  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+
+  "_tuple_args x (_tuple_args y z)" ==
+    "_tuple_args x (_tuple_arg (_tuple y z))"
+
+  "_bind (Some p) e" <= "_bind p (the e)"
+  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
+  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+
+
+end
\ No newline at end of file