| author | wenzelm |
| Fri, 19 Jan 2007 22:08:15 +0100 | |
| changeset 22107 | 926afa3361e1 |
| parent 21404 | eb85850d3eb7 |
| child 22835 | 37d3a984d730 |
| permissions | -rw-r--r-- |
| 15469 | 1 |
(* Title: HOL/Library/OptionalSugar.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klain, Tobias Nipkow |
|
4 |
Copyright 2005 NICTA and TUM |
|
5 |
*) |
|
| 15476 | 6 |
(*<*) |
| 15469 | 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 *) |
|
| 21210 | 20 |
notation (tab output) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
21 |
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
|
| 19674 | 22 |
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
|
| 15469 | 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 |
||
| 15476 | 37 |
end |
38 |
(*>*) |