src/Pure/General/basics.ML
2007-07-03 wenzelm 2007-07-03 tuned;
2007-06-13 wenzelm 2007-06-13 tuned;
2007-06-03 wenzelm 2007-06-03 moved flip to library.ML; removed unused dest/unfold/unfold_rev; simplified fold/fold_rev/fold_map;
2007-05-11 wenzelm 2007-05-11 tuned;
2007-05-11 krauss 2007-05-11 added fun flip f x y = f y x
2006-11-16 wenzelm 2006-11-16 Fundamental concepts.