example theory involving unicode characters (utf-8 encoding);

1 files changed, 69 insertions, 0 deletions

diff --git a/etc/isar/Unicode.thy b/etc/isar/Unicode.thy
new file mode 100644
index 00000000..574df9ce
--- /dev/null
+++ b/etc/isar/Unicode.thy
@@ -0,0 +1,69 @@
+(* -*- coding: utf-8 -*- *)
+
+(*
+  Example theory involving unicode characters (utf-8 encoding) -- both
+  formal and informal ones.
+
+  (Not fully supported, yet.)
+*)
+
+theory Unicode
+imports Main
+begin
+
+text {* The Hebrew Alef-Bet (א-ב). *}
+
+datatype alef_bet =
+    Alef    ("א")
+  | Bet     ("ב")
+  | Gimel   ("ג")
+  | Dalet   ("ד")
+  | He      ("ה")
+  | Vav     ("ו")
+  | Zayin   ("ז")
+  | Het     ("ח")
+  | Tet     ("ט")
+  | Yod     ("י")
+  | Kaf     ("כ")
+  | Lamed   ("ל")
+  | Mem     ("מ")
+  | Nun     ("נ")
+  | Samekh  ("ס")
+  | Ayin    ("ע")
+  | Pe      ("פ")
+  | Tsadi   ("צ")
+  | Qof     ("ק")
+  | Resh    ("ר")
+  | Shin    ("ש")
+  | Tav     ("ת")
+
+
+text {* Interpreting Hebrew letters as numbers. *}
+
+consts
+  mispar :: "alef_bet => nat"
+primrec
+  "mispar א = 1"
+  "mispar ב = 2"
+  "mispar ג = 3"
+  "mispar ד = 4"
+  "mispar ה = 5"
+  "mispar ו = 6"
+  "mispar ז = 7"
+  "mispar ח = 8"
+  "mispar ט = 9"
+  "mispar י = 10"
+  "mispar כ = 20"
+  "mispar ל = 30"
+  "mispar מ = 40"
+  "mispar נ = 50"
+  "mispar ס = 60"
+  "mispar ע = 70"
+  "mispar פ = 80"
+  "mispar צ = 90"
+  "mispar ק = 100"
+  "mispar ר = 200"
+  "mispar ש = 300"
+  "mispar ת = 400"
+
+end