Wed, 25 Mar 2015 17:51:34 +0100 blanchet more multiset theorems
Wed, 25 Mar 2015 14:39:40 +0100 wenzelm semantic completion for @{system_option};
Wed, 25 Mar 2015 13:45:52 +0100 wenzelm clarified position;
Wed, 25 Mar 2015 13:31:47 +0100 wenzelm HOL-SPARK .prv files are subject to system option spark_prv;
Wed, 25 Mar 2015 11:39:52 +0100 wenzelm tuned signature;
Wed, 25 Mar 2015 10:59:28 +0100 wenzelm NEWS;
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Wed, 25 Mar 2015 10:41:53 +0100 wenzelm proper signature;
Wed, 25 Mar 2015 00:22:10 +0100 wenzelm dummies may depend on goal params as well;
Tue, 24 Mar 2015 23:39:42 +0100 wenzelm merged
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
Sun, 22 Mar 2015 13:10:34 +0100 wenzelm tuned;
Sun, 22 Mar 2015 12:45:34 +0100 wenzelm tuned;
Sun, 22 Mar 2015 12:38:41 +0100 wenzelm tuned;
Fri, 20 Mar 2015 22:35:37 +0100 wenzelm tuned;
Fri, 20 Mar 2015 22:18:40 +0100 wenzelm read instantiations uniformly for rules and tactics;
Fri, 20 Mar 2015 21:16:42 +0100 wenzelm removed presumably pointless detail;
Fri, 20 Mar 2015 20:48:33 +0100 wenzelm tuned;
Fri, 20 Mar 2015 20:20:21 +0100 wenzelm tuned;
Fri, 20 Mar 2015 19:05:03 +0100 wenzelm make SML/NJ happy;
Fri, 20 Mar 2015 16:18:20 +0000 paulson Merge
Fri, 20 Mar 2015 16:11:28 +0000 paulson tweaked a few slow or very ugly proofs
Fri, 20 Mar 2015 16:18:28 +0100 wenzelm merged
Fri, 20 Mar 2015 14:48:04 +0100 wenzelm tuned signature;
Fri, 20 Mar 2015 11:53:22 +0100 wenzelm tuned;
Fri, 20 Mar 2015 11:48:34 +0100 wenzelm tuned signature;
Fri, 20 Mar 2015 11:23:32 +0100 wenzelm tuned;
Fri, 20 Mar 2015 11:09:08 +0100 wenzelm tuned -- prepare instantiation more uniformly;
Fri, 20 Mar 2015 14:06:15 +0000 paulson Merge
Fri, 20 Mar 2015 14:00:22 +0000 paulson fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
Thu, 19 Mar 2015 22:31:23 +0100 wenzelm merged
Thu, 19 Mar 2015 22:30:57 +0100 wenzelm more position information;
Thu, 19 Mar 2015 17:25:57 +0100 wenzelm misc tuning;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip