# HG changeset patch # User wenzelm # Date 850223771 -3600 # Node ID 8100f00e895052f6fb70e84165f5859cb7f3579f # Parent d394336997cff8d450078a77e031273bf820517f removed ambiguous symbols syntax; diff -r d394336997cf -r 8100f00e8950 src/HOL/List.thy --- a/src/HOL/List.thy Tue Dec 10 14:09:32 1996 +0100 +++ b/src/HOL/List.thy Tue Dec 10 14:16:11 1996 +0100 @@ -47,9 +47,6 @@ syntax (symbols) "op #" :: ['a, 'a list] => 'a list (infixr "\\" 65) - "op @" :: ['a list, 'a list] => 'a list (infixr "\\" 65) - "op mem" :: ['a, 'a list] => bool (infixl "\\" 55) - "@Alls" :: [idt, 'a list, bool] => bool ("(2\\ _\\_./ _)" 10) "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_\\_ ./ _])")