| 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 |
| Wed, 22 Aug 2012 21:06:26 +0200 | wenzelm | tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction; | changeset | files |
| Wed, 22 Aug 2012 21:02:02 +0200 | wenzelm | discontinued separate list of required files -- maintain only provided files as they occur at runtime; | changeset | files |
| Wed, 22 Aug 2012 18:04:30 +0200 | wenzelm | find files via load commands within theory text; | changeset | files |
| Wed, 22 Aug 2012 16:24:52 +0200 | wenzelm | clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself; | changeset | files |