diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2011-09-28 09:35:01 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2011-09-28 09:35:01 +0000 |
| commit | 75a9e6fa64913e49e55557a6db1b50e8dbc7d25f (patch) | |
| tree | c78cd5b7c16f86e6aa65e4172a88110181bd75c2 /etc/isar/Unicode.thy | |
| parent | be1b30498101ed929f03eb3548359dba1713e8aa (diff) | |
updated tests to Isabelle2011-1;
Diffstat (limited to 'etc/isar/Unicode.thy')
| -rw-r--r-- | etc/isar/Unicode.thy | 47 |
1 files changed, 23 insertions, 24 deletions
diff --git a/etc/isar/Unicode.thy b/etc/isar/Unicode.thy index 0305091b..95140e6a 100644 --- a/etc/isar/Unicode.thy +++ b/etc/isar/Unicode.thy @@ -40,31 +40,30 @@ thm alef_bet.induct 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 |