src/HOL/List.thy
changeset 14565 c6dc17aab88a
parent 14538 1d9d75a8efae
child 14589 feae7b5fd425
     1.1 --- a/src/HOL/List.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -71,6 +71,8 @@
     1.4  
     1.5  syntax (xsymbols)
     1.6    "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
     1.7 +syntax (HTML output)
     1.8 +  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
     1.9  
    1.10  
    1.11  text {*