src/Pure/library.ML
changeset 25752 374446e93558
parent 25702 a61554b1e7a9
child 25797 b293e3ed3cad
     1.1 --- a/src/Pure/library.ML	Tue Jan 01 07:28:20 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Jan 01 16:09:26 2008 +0100
     1.3 @@ -315,17 +315,8 @@
     1.4  fun p orf q = fn x => p x orelse q x;
     1.5  fun p andf q = fn x => p x andalso q x;
     1.6  
     1.7 -(*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
     1.8 -fun exists (pred: 'a -> bool) : 'a list -> bool =
     1.9 -  let fun boolf [] = false
    1.10 -        | boolf (x :: xs) = pred x orelse boolf xs
    1.11 -  in boolf end;
    1.12 -
    1.13 -(*forall pred [x1, ..., xn] ===> pred x1 andalso ... andalso pred xn*)
    1.14 -fun forall (pred: 'a -> bool) : 'a list -> bool =
    1.15 -  let fun boolf [] = true
    1.16 -        | boolf (x :: xs) = pred x andalso boolf xs
    1.17 -  in boolf end;
    1.18 +val exists = List.exists;
    1.19 +val forall = List.all;
    1.20  
    1.21  
    1.22  (* flags *)