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