src/HOL/Library/OptionalSugar.thy
author wenzelm
Tue Nov 07 11:47:57 2006 +0100 (2006-11-07)
changeset 21210 c17fd2df4e9e
parent 19674 22b635240905
child 21404 eb85850d3eb7
permissions -rw-r--r--
renamed 'const_syntax' to 'notation';
     1 (*  Title:      HOL/Library/OptionalSugar.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klain, Tobias Nipkow
     4     Copyright   2005 NICTA and TUM
     5 *)
     6 (*<*)
     7 theory OptionalSugar
     8 imports LaTeXsugar
     9 begin
    10 
    11 (* append *)
    12 syntax (latex output)
    13   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    14 translations
    15   "appendL xs ys" <= "xs @ ys" 
    16   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
    17 
    18 
    19 (* aligning equations *)
    20 notation (tab output)
    21   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
    22   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    23 
    24 (* Let *)
    25 translations 
    26   "_bind (p,DUMMY) e" <= "_bind p (fst e)"
    27   "_bind (DUMMY,p) e" <= "_bind p (snd e)"
    28 
    29   "_tuple_args x (_tuple_args y z)" ==
    30     "_tuple_args x (_tuple_arg (_tuple y z))"
    31 
    32   "_bind (Some p) e" <= "_bind p (the e)"
    33   "_bind (p#DUMMY) e" <= "_bind p (hd e)"
    34   "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    35 
    36 
    37 end
    38 (*>*)