| Thu, 19 Mar 2009 11:47:05 +0100 | wenzelm | command 'use', 'ML': apply ML environment to theory and target as well; | changeset | files |
| Thu, 19 Mar 2009 11:44:34 +0100 | wenzelm | added map_contexts (cf. Proof.map_contexts); | changeset | files |
| 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 |