equal
deleted
inserted
replaced
2 |
2 |
3 Example theory involving Unicode characters (UTF-8 encoding) -- both |
3 Example theory involving Unicode characters (UTF-8 encoding) -- both |
4 formal and informal ones. |
4 formal and informal ones. |
5 *) |
5 *) |
6 |
6 |
7 section {* A Hebrew theory *} |
7 section \<open>A Hebrew theory\<close> |
8 |
8 |
9 theory Hebrew |
9 theory Hebrew |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 text {* The Hebrew Alef-Bet (א-ב). *} |
13 text \<open>The Hebrew Alef-Bet (א-ב).\<close> |
14 |
14 |
15 datatype alef_bet = |
15 datatype alef_bet = |
16 Alef ("א") |
16 Alef ("א") |
17 | Bet ("ב") |
17 | Bet ("ב") |
18 | Gimel ("ג") |
18 | Gimel ("ג") |
37 | Tav ("ת") |
37 | Tav ("ת") |
38 |
38 |
39 thm alef_bet.induct |
39 thm alef_bet.induct |
40 |
40 |
41 |
41 |
42 text {* Interpreting Hebrew letters as numbers. *} |
42 text \<open>Interpreting Hebrew letters as numbers.\<close> |
43 |
43 |
44 primrec mispar :: "alef_bet => nat" where |
44 primrec mispar :: "alef_bet => nat" |
|
45 where |
45 "mispar א = 1" |
46 "mispar א = 1" |
46 | "mispar ב = 2" |
47 | "mispar ב = 2" |
47 | "mispar ג = 3" |
48 | "mispar ג = 3" |
48 | "mispar ד = 4" |
49 | "mispar ד = 4" |
49 | "mispar ה = 5" |
50 | "mispar ה = 5" |