Tue, 21 Aug 2012 09:02:29 +0200 abstracted lemmas
nipkow [Tue, 21 Aug 2012 09:02:29 +0200] rev 48893
abstracted lemmas
Wed, 22 Aug 2012 23:22:57 +0200 prefer ML_file over old uses;
wenzelm [Wed, 22 Aug 2012 23:22:57 +0200] rev 48892
prefer ML_file over old uses;
Wed, 22 Aug 2012 22:55:41 +0200 prefer ML_file over old uses;
wenzelm [Wed, 22 Aug 2012 22:55:41 +0200] rev 48891
prefer ML_file over old uses;
Wed, 22 Aug 2012 22:47:16 +0200 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via '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';
Wed, 22 Aug 2012 21:43:17 +0200 add keywords of this node as well (e.g. relevant for Pure.thy);
wenzelm [Wed, 22 Aug 2012 21:43:17 +0200] rev 48889
add keywords of this node as well (e.g. relevant for Pure.thy);
Wed, 22 Aug 2012 21:28:33 +0200 tuned;
wenzelm [Wed, 22 Aug 2012 21:28:33 +0200] rev 48888
tuned;
Wed, 22 Aug 2012 21:06:26 +0200 tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
wenzelm [Wed, 22 Aug 2012 21:06:26 +0200] rev 48887
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
Wed, 22 Aug 2012 21:02:02 +0200 discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm [Wed, 22 Aug 2012 21:02:02 +0200] rev 48886
discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;
Wed, 22 Aug 2012 18:04:30 +0200 find files via load commands within theory text;
wenzelm [Wed, 22 Aug 2012 18:04:30 +0200] rev 48885
find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;
Wed, 22 Aug 2012 16:24:52 +0200 clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm [Wed, 22 Aug 2012 16:24:52 +0200] rev 48884
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip