# 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 "\\<bullet>" 65)
-  "op @"      :: ['a list, 'a list] => 'a list            (infixr "\\<circ>" 65)
-  "op mem"    :: ['a, 'a list] => bool                    (infixl "\\<in>" 55)
-  "@Alls"     :: [idt, 'a list, bool] => bool             ("(2\\<forall> _\\<in>_./ _)" 10)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")