src/Pure/General/same.ML
Thu, 16 Jul 2009 21:28:39 +0200 wenzelm added map_option;
Thu, 16 Jul 2009 20:15:57 +0200 wenzelm added map;
Thu, 16 Jul 2009 16:24:49 +0200 wenzelm Support for copy-avoiding functions on pure values, at the cost of readability.
less more (0) tip