flipped fold implementation
authornipkow
Mon, 15 Dec 2008 10:16:38 +0100
changeset 29110 476c46e99ada
parent 29109 389ebed8b98e
child 29111 d2b60c49a713
flipped fold implementation
src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Thu Dec 11 08:59:03 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Dec 15 10:16:38 2008 +0100
@@ -275,7 +275,6 @@
   Ball ("{*Blall*}")
   Bex ("{*Blex*}")
   filter_set ("{*filter*}")
-  fold ("{* foldl *}")
-
+  fold ("{* foldl o flip *}")
 
 end