--- a/src/HOL/ex/Hebrew.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/Hebrew.thy Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
(* -*- coding: utf-8 -*- :encoding=utf-8:
- ID: $Id$
Author: Makarius
Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -43,31 +42,29 @@
text {* Interpreting Hebrew letters as numbers. *}
-consts
- mispar :: "alef_bet => nat"
-primrec
+primrec mispar :: "alef_bet => nat" where
"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"
+| "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