src/HOL/List.thy
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_ :=/ _)")