| Wed, 17 Sep 2008 21:27:44 +0200 | wenzelm | ML_Context.evaluate: proper context (for ML environment); | changeset | files |
| Wed, 17 Sep 2008 21:27:43 +0200 | wenzelm | ML_Context.evaluate: proper context (for ML environment); | changeset | files |
| Wed, 17 Sep 2008 21:27:38 +0200 | wenzelm | simplified ML_Context.eval_in -- expect immutable Proof.context value; | changeset | files |
| Wed, 17 Sep 2008 21:27:36 +0200 | wenzelm | proper thm antiquotations within ML solve obscure context problems (due to update of ML environment); | changeset | files |