changeset 2271 | 7c4744ed8fc3 |
parent 2243 | 3ebeaaacfbd1 |
child 2303 | 84ed9e0d7c50 |
--- a/src/Pure/library.ML Thu Nov 28 12:31:33 1996 +0100 +++ b/src/Pure/library.ML Thu Nov 28 12:36:31 1996 +0100 @@ -112,6 +112,10 @@ fun andl [] = true | andl (x :: xs) = x andalso andl xs; +(*Needed because several object-logics declare the theory, therefore structure, + List.*) +structure List_ = List; + (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*) fun exists (pred: 'a -> bool) : 'a list -> bool = let fun boolf [] = false