src/HOL/HOL.thy

   "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
   "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
-(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
+(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
 
 syntax (xsymbols output)
   "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
 
 syntax (HTML output)