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