Sat, 08 Nov 2014 15:01:05 +0100 wenzelm recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
Sat, 08 Nov 2014 12:15:40 +0100 wenzelm more direct type equality;
Sat, 08 Nov 2014 09:19:57 +0100 haftmann reverted commit accident from 994fe0ba8335
Sat, 08 Nov 2014 09:16:47 +0100 haftmann less space-wasting serialization setup: highest cell of array has been unused so far
Fri, 07 Nov 2014 23:35:13 +0100 wenzelm tuned outline;
Fri, 07 Nov 2014 22:33:54 +0100 wenzelm tuned syntax -- separate tokens;
Fri, 07 Nov 2014 22:15:51 +0100 wenzelm eliminated pointless check -- command definitions are subject to theory context;
Fri, 07 Nov 2014 20:43:13 +0100 wenzelm merged
Fri, 07 Nov 2014 20:06:18 +0100 wenzelm prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
Fri, 07 Nov 2014 19:47:05 +0100 wenzelm tuned markup;
Fri, 07 Nov 2014 17:43:50 +0100 wenzelm tuned;
Fri, 07 Nov 2014 17:31:01 +0100 wenzelm clarified keyword categories;
Fri, 07 Nov 2014 16:55:09 +0100 wenzelm tuned signature;
Fri, 07 Nov 2014 16:51:36 +0100 wenzelm tuned;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Fri, 07 Nov 2014 16:22:25 +0100 wenzelm proper import for command 'permanent_interpretation';
Fri, 07 Nov 2014 16:13:05 +0100 wenzelm proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
Fri, 07 Nov 2014 15:19:30 +0100 wenzelm more accurate keywords;
Thu, 06 Nov 2014 16:10:33 +0100 wenzelm tuned signature;
Thu, 06 Nov 2014 15:47:04 +0100 wenzelm more explicit Keyword.keywords;
Thu, 06 Nov 2014 15:42:34 +0100 wenzelm proper Keyword.keywords (cf. 82a71046dce8);
Thu, 06 Nov 2014 15:05:15 +0100 wenzelm prefer explicit Keyword.keywords (cf. 82a71046dce8);
Thu, 06 Nov 2014 13:44:14 +0100 wenzelm tuned signature;
Thu, 06 Nov 2014 13:36:19 +0100 wenzelm prefer explicit Keyword.keywords;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 tip