| changeset 36176 | 3fe7e97ccca8 |
| parent 36112 | 7fa17a225852 |
| child 36274 | 42bd879dc1b0 |
--- a/src/HOL/Library/Dlist.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Fri Apr 16 21:28:09 2010 +0200 @@ -247,6 +247,6 @@ end -hide (open) const member fold empty insert remove map filter null member length fold +hide_const (open) member fold empty insert remove map filter null member length fold end