wenzelm [Thu, 23 Aug 2012 11:58:10 +0200] rev 48896
simplified Thy_Load.provide: do not store full path;
wenzelm [Wed, 22 Aug 2012 23:45:49 +0200] rev 48895
prefer ML_file over old uses;
updated generated files;
wenzelm [Wed, 22 Aug 2012 23:23:48 +0200] rev 48894
merged
nipkow [Tue, 21 Aug 2012 09:02:29 +0200] rev 48893
abstracted lemmas
wenzelm [Wed, 22 Aug 2012 23:22:57 +0200] rev 48892
prefer ML_file over old uses;
wenzelm [Wed, 22 Aug 2012 22:55:41 +0200] rev 48891
prefer ML_file over old uses;
wenzelm [Wed, 22 Aug 2012 22:47:16 +0200] rev 48890
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm [Wed, 22 Aug 2012 21:43:17 +0200] rev 48889
add keywords of this node as well (e.g. relevant for Pure.thy);
wenzelm [Wed, 22 Aug 2012 21:28:33 +0200] rev 48888
tuned;
wenzelm [Wed, 22 Aug 2012 21:06:26 +0200] rev 48887
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;