Tue, 24 Mar 2015 23:37:05 +0100 wenzelm proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;
Tue, 24 Mar 2015 21:54:25 +0100 wenzelm clarified case_tac fixes and context;
Tue, 24 Mar 2015 20:07:27 +0100 wenzelm clarified name;
Tue, 24 Mar 2015 19:43:23 +0100 wenzelm option to control old-style schematic mode;
Tue, 24 Mar 2015 18:36:29 +0100 wenzelm clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
Tue, 24 Mar 2015 16:17:07 +0100 wenzelm tuned;
Tue, 24 Mar 2015 16:16:48 +0100 wenzelm tuned proof;
Tue, 24 Mar 2015 15:57:51 +0100 wenzelm admit dummy patterns in instantiations;
Tue, 24 Mar 2015 11:53:18 +0100 wenzelm clarified input source;
Tue, 24 Mar 2015 18:10:56 +0100 blanchet tuning
Tue, 24 Mar 2015 18:10:56 +0100 blanchet reordered properties
Mon, 23 Mar 2015 23:16:40 +0100 wenzelm NEWS;
Mon, 23 Mar 2015 23:12:33 +0100 wenzelm tuned proof;
Mon, 23 Mar 2015 22:57:04 +0100 wenzelm implicit goal parameters are improper;
Mon, 23 Mar 2015 21:14:49 +0100 wenzelm merged
Mon, 23 Mar 2015 21:05:17 +0100 wenzelm prefer local fixes;
Mon, 23 Mar 2015 19:43:03 +0100 wenzelm local fixes may depend on goal params;
Mon, 23 Mar 2015 17:07:43 +0100 wenzelm tuned;
Mon, 23 Mar 2015 17:01:47 +0100 wenzelm clarified syntax category "fixes";
Mon, 23 Mar 2015 16:10:32 +0100 wenzelm tuned signature;
Mon, 23 Mar 2015 15:55:41 +0100 wenzelm tuned syntax diagrams -- no duplication of "target";
Mon, 23 Mar 2015 15:54:41 +0100 wenzelm tuned;
Mon, 23 Mar 2015 14:56:52 +0100 wenzelm tuned;
Mon, 23 Mar 2015 13:30:59 +0100 wenzelm support 'for' fixes in rule_tac etc.;
Mon, 23 Mar 2015 15:08:02 +0100 hoelzl fix parameter order of NO_MATCH
Mon, 23 Mar 2015 10:16:20 +0100 hoelzl add measurable_submarkov
Mon, 23 Mar 2015 08:45:54 +0100 nipkow BT subsumed by Library/Tree
Mon, 23 Mar 2015 07:36:27 +0100 nipkow added funs and lemmas
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 tip