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