Thu, 19 Mar 2009 11:20:22 +0100 | wenzelm | tuned; | changeset | files |
Wed, 18 Mar 2009 22:41:15 +0100 | wenzelm | generalized ML_Context.inherit_env; | changeset | files |
Wed, 18 Mar 2009 22:41:14 +0100 | wenzelm | more precise type Symbol_Pos.text; | changeset | files |
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 |
Wed, 18 Mar 2009 19:11:26 +0100 | wenzelm | reduced verbosity; | changeset | files |