# HG changeset patch
# User wenzelm
# Date 1126797422 -7200
# Node ID c9e9d2a2fc72e0aa4905de8a0f2fab5844baabfc
# Parent  89ccb379942843f9cb4965298be46a59e62336e5
The Hebrew Alef-Bet -- Unicode example;

diff -r 89ccb3799428 -r c9e9d2a2fc72 src/HOL/ex/Hebrew.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Hebrew.thy	Thu Sep 15 17:17:02 2005 +0200
@@ -0,0 +1,75 @@
+(* -*- coding: utf-8 -*-  
+    ID:         $Id$
+    Author:     Makarius
+
+Example theory involving Unicode characters (UTF-8 encoding) -- both
+formal and informal ones.
+*)
+
+theory Hebrew
+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     ("ת")
+
+thm alef_bet.induct
+
+
+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"
+
+thm mispar.simps
+
+lemma "mispar ק + mispar ל + mispar ה = 135"
+  by simp
+
+end