author | wenzelm |
Tue, 10 Dec 1996 14:16:11 +0100 | |
changeset 2369 | 8100f00e8950 |
parent 2368 | d394336997cf |
child 2370 | 5f9607d293f5 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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>_ ./ _])")