# HG changeset patch # User nipkow # Date 1229332598 -3600 # Node ID 476c46e99ada98eddc805ca1781c196fb98d5ee6 # Parent 389ebed8b98e94421a99c8d54b265893e1f2bf12 flipped fold implementation diff -r 389ebed8b98e -r 476c46e99ada 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