--- a/src/HOL/ex/Hebrew.thy Sat Nov 22 14:13:36 2014 +0100
+++ b/src/HOL/ex/Hebrew.thy Sat Nov 22 14:57:04 2014 +0100
@@ -4,13 +4,13 @@
formal and informal ones.
*)
-section {* A Hebrew theory *}
+section \<open>A Hebrew theory\<close>
theory Hebrew
imports Main
begin
-text {* The Hebrew Alef-Bet (א-ב). *}
+text \<open>The Hebrew Alef-Bet (א-ב).\<close>
datatype alef_bet =
Alef ("א")
@@ -39,9 +39,10 @@
thm alef_bet.induct
-text {* Interpreting Hebrew letters as numbers. *}
+text \<open>Interpreting Hebrew letters as numbers.\<close>
-primrec mispar :: "alef_bet => nat" where
+primrec mispar :: "alef_bet => nat"
+where
"mispar א = 1"
| "mispar ב = 2"
| "mispar ג = 3"