equal
deleted
inserted
replaced
|
1 theory OptionalSugar |
|
2 imports LaTeXsugar |
|
3 begin |
|
4 |
|
5 (* append *) |
|
6 syntax (latex output) |
|
7 "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65) |
|
8 translations |
|
9 "appendL xs ys" <= "xs @ ys" |
|
10 "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" |
|
11 |
|
12 |
|
13 (* and *) |
|
14 syntax (latex output) |
|
15 "_andL" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<^raw:\isasymand>" 35) |
|
16 translations |
|
17 "_andL A B" <= "A \<and> B" |
|
18 "_andL (_andL A B) C" <= "_andL A (_andL B C)" |
|
19 |
|
20 |
|
21 (* aligning equations *) |
|
22 syntax (tab output) |
|
23 "op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) |
|
24 "==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
|
25 |
|
26 (* Let *) |
|
27 translations |
|
28 "_bind (p,DUMMY) e" <= "_bind p (fst e)" |
|
29 "_bind (DUMMY,p) e" <= "_bind p (snd e)" |
|
30 |
|
31 "_tuple_args x (_tuple_args y z)" == |
|
32 "_tuple_args x (_tuple_arg (_tuple y z))" |
|
33 |
|
34 "_bind (Some p) e" <= "_bind p (the e)" |
|
35 "_bind (p#DUMMY) e" <= "_bind p (hd e)" |
|
36 "_bind (DUMMY#p) e" <= "_bind p (tl e)" |
|
37 |
|
38 |
|
39 end |