| Thu, 23 Aug 2012 11:58:10 +0200 | wenzelm | simplified Thy_Load.provide: do not store full path; | changeset | files |
| Wed, 22 Aug 2012 23:45:49 +0200 | wenzelm | prefer ML_file over old uses; | changeset | files |
| Wed, 22 Aug 2012 23:23:48 +0200 | wenzelm | merged | changeset | files |
| Tue, 21 Aug 2012 09:02:29 +0200 | nipkow | abstracted lemmas | changeset | files |
| Wed, 22 Aug 2012 23:22:57 +0200 | wenzelm | prefer ML_file over old uses; | changeset | files |
| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | changeset | files |
| 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 |