| Wed, 22 Aug 2012 22:47:16 +0200 | wenzelm | 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses'; | changeset | files |
| Wed, 22 Aug 2012 21:43:17 +0200 | wenzelm | add keywords of this node as well (e.g. relevant for Pure.thy); | changeset | files |
| Wed, 22 Aug 2012 21:28:33 +0200 | wenzelm | tuned; | changeset | files |