# HG changeset patch
# User wenzelm
# Date 1459542258 -7200
# Node ID 4b8f08de279270c5ee664f1f4a13ef89cde04b37
# Parent  288c309df28d592acd2796df9f43d900c2be6272
explicit warning about bidi uncertainty in Unicode;

diff -r 288c309df28d -r 4b8f08de2792 src/HOL/ex/Hebrew.thy
--- a/src/HOL/ex/Hebrew.thy	Fri Apr 01 22:20:03 2016 +0200
+++ b/src/HOL/ex/Hebrew.thy	Fri Apr 01 22:24:18 2016 +0200
@@ -10,7 +10,20 @@
 imports Main
 begin
 
-text \<open>The Hebrew Alef-Bet (א-ב).\<close>
+subsection \<open>Warning: formal Unicode considered harmful\<close>
+
+text \<open>
+  Important note: editors or browsers that implement the \<^emph>\<open>Unicode
+  Bidirectional Algorithm\<close> correctly (!) will display the following mix of
+  left-to-right versus right-to-left characters in a way that is logical
+  nonsense.
+
+  To avoid such uncertainty, formal notation should be restricted to
+  well-known Isabelle symbols and their controlled rendering (in Unicode or
+  LaTeX).
+\<close>
+
+subsection \<open>The Hebrew Alef-Bet (א-ב).\<close>
 
 datatype alef_bet =
     Alef    ("א")
@@ -39,9 +52,9 @@
 thm alef_bet.induct
 
 
-text \<open>Interpreting Hebrew letters as numbers.\<close>
+subsection \<open>Interpreting Hebrew letters as numbers.\<close>
 
-primrec mispar :: "alef_bet => nat"
+primrec mispar :: "alef_bet \<Rightarrow> nat"
 where
   "mispar א = 1"
 | "mispar ב = 2"