changeset 9341 | 40bab6613000 |
parent 9336 | 9ae89b9ce206 |
child 9355 | 1b2cd40579c6 |
--- a/src/HOL/List.thy Fri Jul 14 16:27:45 2000 +0200 +++ b/src/HOL/List.thy Fri Jul 14 16:28:49 2000 +0200 @@ -43,7 +43,7 @@ "@list" :: args => 'a list ("[(_)]") (* Special syntax for filter *) - "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_ ./ _])") + "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_./ _])") (* list update *) "_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)")