| Wed, 17 Sep 2008 21:27:34 +0200 | wenzelm | simplified ML_Context.eval_in -- expect immutable Proof.context value; | changeset | files |
| Wed, 17 Sep 2008 21:27:32 +0200 | wenzelm | explicit handling of ML environment within generic context; | changeset | files |
| Wed, 17 Sep 2008 21:27:31 +0200 | wenzelm | added ML_prf; | changeset | files |
| Wed, 17 Sep 2008 21:27:24 +0200 | wenzelm | use_text/use_file now depend on explicit ML name space; | changeset | files |
| Wed, 17 Sep 2008 21:27:22 +0200 | wenzelm | ML name space -- dummy version of Poly/ML 5.2 facility. | changeset | files |
| Wed, 17 Sep 2008 21:27:20 +0200 | wenzelm | added ML-Systems/ml_name_space.ML; | changeset | files |
| Wed, 17 Sep 2008 21:27:18 +0200 | wenzelm | use ML_prf within proofs; | changeset | files |