| author | nipkow |
| Fri, 25 May 2007 18:08:34 +0200 | |
| changeset 23100 | 1c84d7294d5b |
| parent 22835 | 37d3a984d730 |
| child 29494 | a189c6274c7a |
| 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 |
||
| 22835 | 11 |
(* set *) |
12 |
translations |
|
13 |
"xs" <= "set xs" |
|
14 |
||
| 15469 | 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 *) |
|
| 21210 | 24 |
notation (tab output) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
25 |
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
|
| 19674 | 26 |
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
|
| 15469 | 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 |
||
| 15476 | 41 |
end |
42 |
(*>*) |