--- a/src/HOL/Tools/prop_logic.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Tools/prop_logic.ML Thu Mar 03 12:43:01 2005 +0100
@@ -275,7 +275,7 @@
(* prop_formula list -> prop_formula *)
- fun exists xs = foldl SOr (False, xs);
+ fun exists xs = Library.foldl SOr (False, xs);
(* ------------------------------------------------------------------------- *)
(* all: computes the conjunction over a list 'xs' of propositional formulas *)
@@ -283,7 +283,7 @@
(* prop_formula list -> prop_formula *)
- fun all xs = foldl SAnd (True, xs);
+ fun all xs = Library.foldl SAnd (True, xs);
(* ------------------------------------------------------------------------- *)
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *)