# HG changeset patch
# User wenzelm
# Date 854122348 -3600
# Node ID 470bc495373e75fcfff1da360a87419f6939787d
# Parent  fe15e3fcccf063ba75e6fcd97ba21cc6a730e211
changed case symbol to \<Rightarrow>;

diff -r fe15e3fcccf0 -r 470bc495373e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jan 23 18:16:12 1997 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 24 17:12:28 1997 +0100
@@ -123,7 +123,7 @@
   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
+  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
 
 syntax (symbols output)
   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)