src/HOL/List.thy
changeset 2369 8100f00e8950
parent 2262 c7ee913746fd
child 2512 0231e4f467f2
--- 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>_ ./ _])")