Wed, 18 Mar 2009 20:03:01 +0100 | wenzelm | Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion; | changeset | files |
Wed, 18 Mar 2009 19:11:26 +0100 | wenzelm | reduced verbosity; | changeset | files |
Wed, 18 Mar 2009 15:23:52 +0100 | haftmann | made SML/NJ happy | changeset | files |
Wed, 18 Mar 2009 11:57:28 +0100 | haftmann | tuned interpunctation | changeset | files |