src/HOL/Library/OptionalSugar.thy
author nipkow
Thu Jan 27 13:33:21 2005 +0100 (2005-01-27)
changeset 15476 b8cb20cc0c0b
parent 15469 f5d22f504ab9
child 19674 22b635240905
permissions -rw-r--r--
fixed bugs
     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 syntax (tab output)
    21   "op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
    22   "==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^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 (*>*)