changeset 1374 | 5e407f2a3323 |
parent 1335 | 5e1c0540f285 |
child 1476 | 608483c2122a |
1373:f061d2435d63 | 1374:5e407f2a3323 |
---|---|
7 *) |
7 *) |
8 |
8 |
9 Examples = Hoare + Arith2 + |
9 Examples = Hoare + Arith2 + |
10 |
10 |
11 syntax |
11 syntax |
12 "@1" :: "nat" ("1") |
12 "@1" :: nat ("1") |
13 "@2" :: "nat" ("2") |
13 "@2" :: nat ("2") |
14 |
14 |
15 translations |
15 translations |
16 "1" == "Suc(0)" |
16 "1" == "Suc(0)" |
17 "2" == "Suc(Suc(0))" |
17 "2" == "Suc(Suc(0))" |
18 end |
18 end |