src/HOL/Library/OptionalSugar.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22835 37d3a984d730
child 29494 a189c6274c7a
permissions -rw-r--r--
tuned Proof
     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 (* set *)
    12 translations
    13   "xs" <= "set xs"
    14 
    15 (* append *)
    16 syntax (latex output)
    17   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
    18 translations
    19   "appendL xs ys" <= "xs @ ys" 
    20   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
    21 
    22 
    23 (* aligning equations *)
    24 notation (tab output)
    25   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
    26   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    27 
    28 (* Let *)
    29 translations 
    30   "_bind (p,DUMMY) e" <= "_bind p (fst e)"
    31   "_bind (DUMMY,p) e" <= "_bind p (snd e)"
    32 
    33   "_tuple_args x (_tuple_args y z)" ==
    34     "_tuple_args x (_tuple_arg (_tuple y z))"
    35 
    36   "_bind (Some p) e" <= "_bind p (the e)"
    37   "_bind (p#DUMMY) e" <= "_bind p (hd e)"
    38   "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    39 
    40 
    41 end
    42 (*>*)