| Wed, 17 Sep 2008 21:27:18 +0200 | wenzelm | use ML_prf within proofs; | changeset | files |
| Wed, 17 Sep 2008 21:27:17 +0200 | wenzelm | local @{context}; | changeset | files |
| Wed, 17 Sep 2008 21:27:14 +0200 | wenzelm | moved global ML bindings to global place; | changeset | files |
| Wed, 17 Sep 2008 21:27:08 +0200 | wenzelm | back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block; | changeset | files |
| Wed, 17 Sep 2008 21:27:03 +0200 | wenzelm | updated generated file; | changeset | files |
| Wed, 17 Sep 2008 15:59:23 +0200 | krauss | wf_finite_psubset[simp], in_finite_psubset[simp] | changeset | files |
| Wed, 17 Sep 2008 15:21:30 +0200 | ballarin | Public interface to interpretation morphism. | changeset | files |