| changeset 2291 | fbd14a05fb88 |
| parent 2278 | d63ffafce255 |
| child 2394 | 91d8abf108be |
| 2290:e5c08f8b483b | 2291:fbd14a05fb88 |
|---|---|
41 |
41 |
42 tr_when_def "tr_when == |
42 tr_when_def "tr_when == |
43 (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))" |
43 (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))" |
44 |
44 |
45 (* start 8bit 1 *) |
45 (* start 8bit 1 *) |
46 syntax |
|
47 "GeqTT" :: "tr => bool" ("(Å_Æ)") |
|
48 "GeqFF" :: "tr => bool" ("(Ç_È)") |
|
49 |
|
50 translations |
|
51 "ÅxÆ" == "x = TT" |
|
52 "ÇxÈ" == "x = FF" |
|
53 |
|
54 (* end 8bit 1 *) |
46 (* end 8bit 1 *) |
55 |
47 |
56 |
48 |
57 end |
49 end |