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>_ ./ _])")