| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 58889 | 5b7a9633cfa8 |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 text {* The Hebrew Alef-Bet (א-ב). *} |
13 text {* The Hebrew Alef-Bet (א-ב). *} |
14 |
14 |
15 datatype_new alef_bet = |
15 datatype alef_bet = |
16 Alef ("א") |
16 Alef ("א") |
17 | Bet ("ב") |
17 | Bet ("ב") |
18 | Gimel ("ג") |
18 | Gimel ("ג") |
19 | Dalet ("ד") |
19 | Dalet ("ד") |
20 | He ("ה") |
20 | He ("ה") |