removed separate exists/forall code;
authorwenzelm
Tue, 01 Jan 2008 16:09:26 +0100
changeset 25752 374446e93558
parent 25751 a4e69ce247e0
child 25753 99c9fc5e11f2
removed separate exists/forall code;
src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jan 01 07:28:20 2008 +0100
+++ b/src/Pure/library.ML	Tue Jan 01 16:09:26 2008 +0100
@@ -315,17 +315,8 @@
 fun p orf q = fn x => p x orelse q x;
 fun p andf q = fn x => p x andalso q x;
 
-(*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
-fun exists (pred: 'a -> bool) : 'a list -> bool =
-  let fun boolf [] = false
-        | boolf (x :: xs) = pred x orelse boolf xs
-  in boolf end;
-
-(*forall pred [x1, ..., xn] ===> pred x1 andalso ... andalso pred xn*)
-fun forall (pred: 'a -> bool) : 'a list -> bool =
-  let fun boolf [] = true
-        | boolf (x :: xs) = pred x andalso boolf xs
-  in boolf end;
+val exists = List.exists;
+val forall = List.all;
 
 
 (* flags *)