--- a/src/HOL/HOL.thy Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/HOL.thy Mon Jan 26 10:34:02 2004 +0100
@@ -96,7 +96,7 @@
"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)