| Wed, 18 Mar 2009 22:41:14 +0100 | wenzelm | more precise type Symbol_Pos.text; | changeset | files |
| Wed, 18 Mar 2009 21:55:38 +0100 | wenzelm | de-camelized Symbol_Pos; | changeset | files |
| 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 |