| Wed, 12 Mar 2014 22:44:55 +0100 | wenzelm | added ML antiquotation @{here}; | changeset | files |
| Wed, 12 Mar 2014 22:41:04 +0100 | wenzelm | ML_Context.check_antiquotation still required; | changeset | files |
| Wed, 12 Mar 2014 21:58:48 +0100 | wenzelm | simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; | changeset | files |
| Wed, 12 Mar 2014 21:29:46 +0100 | wenzelm | proper base comparison; | changeset | files |
| Wed, 12 Mar 2014 21:28:09 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 12 Mar 2014 17:25:28 +0100 | wenzelm | tuned proofs; | changeset | files |