src/HOL/HOL.thy
changeset 2552 470bc495373e
parent 2393 651fce76c86c
child 2720 3490ef519a56
--- 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)