|
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)
|
|
19674
|
21 |
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
|
|
|
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 |
(*>*)
|