Tue, 14 Feb 2012 20:43:32 +0100 wenzelm method setup;
Tue, 14 Feb 2012 20:09:35 +0100 wenzelm simplified use of tacticals;
Tue, 14 Feb 2012 20:08:59 +0100 wenzelm comment;
Tue, 14 Feb 2012 19:51:39 +0100 wenzelm tuned signature, according to actual usage of these operations;
Tue, 14 Feb 2012 19:29:54 +0100 wenzelm tuned signature;
Tue, 14 Feb 2012 19:18:57 +0100 wenzelm normalized aliases;
Tue, 14 Feb 2012 17:54:08 +0100 wenzelm elininated unused INTLEAVE;
Tue, 14 Feb 2012 17:51:29 +0100 wenzelm eliminated unused rewrite_goal_rule;
Tue, 14 Feb 2012 17:49:47 +0100 wenzelm eliminated unused subgoals_tac;
Tue, 14 Feb 2012 17:26:35 +0100 wenzelm eliminated obsolete aliases;
Tue, 14 Feb 2012 17:11:33 +0100 wenzelm eliminated obsolete aliases;
Tue, 14 Feb 2012 16:59:12 +0100 wenzelm tuned;
Tue, 14 Feb 2012 12:40:55 +0100 wenzelm merged, resolving trivial conflicts;
Tue, 14 Feb 2012 11:16:07 +0100 wenzelm merged;
Sat, 11 Feb 2012 13:41:36 +0100 blanchet new SPASS options
Sat, 11 Feb 2012 12:13:08 +0100 bulwahn making num_mutations a configuration that can be changed with the mutabelle bash command
Sat, 11 Feb 2012 11:36:23 +0100 bulwahn making max_mutants an option that can be changed in the Mutabelle-script
Sat, 11 Feb 2012 11:36:21 +0100 bulwahn increase timeout to 30 seconds; changing mutabelle script
Fri, 10 Feb 2012 17:10:49 +0100 blanchet parse clauses generated from several formulas
Fri, 10 Feb 2012 17:10:47 +0100 blanchet be more gentle when generating KBO weights
Fri, 10 Feb 2012 16:33:58 +0100 blanchet update SPASS slices
Fri, 10 Feb 2012 09:47:59 +0100 Cezary Kaliszyk more specification of the quotient package in IsarRef
Fri, 10 Feb 2012 09:02:51 +0100 Cezary Kaliszyk specification of the quotient package
Thu, 09 Feb 2012 16:00:04 +0100 blanchet tune KBO weight code
Thu, 09 Feb 2012 14:42:18 +0100 blanchet minor DFG fix
Thu, 09 Feb 2012 14:35:27 +0100 blanchet new SPASS slices
Thu, 09 Feb 2012 14:04:17 +0100 blanchet improved KBO weights -- beware of explicit applications
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems
Thu, 09 Feb 2012 09:36:30 +0100 Cezary Kaliszyk Generalize the compositional preservation theorems
Wed, 08 Feb 2012 01:49:33 +0100 blanchet use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
Wed, 08 Feb 2012 00:55:06 +0100 blanchet removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
Wed, 08 Feb 2012 00:05:22 +0100 blanchet beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
Mon, 06 Feb 2012 23:01:02 +0100 blanchet fixed arity error
Mon, 06 Feb 2012 23:01:02 +0100 blanchet tuning
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding
Sun, 05 Feb 2012 17:43:15 +0100 bulwahn adding some forbidden constant names for mutabelle
Sun, 05 Feb 2012 17:43:14 +0100 bulwahn mutabelle ignores theorems with internal constants
Sun, 05 Feb 2012 17:09:21 +0100 nipkow tuned
Sun, 05 Feb 2012 16:53:20 +0100 nipkow merged
Sun, 05 Feb 2012 16:53:11 +0100 nipkow simplified code generation
Sun, 05 Feb 2012 13:28:51 +0100 blanchet remove option that's on by default
Sun, 05 Feb 2012 12:27:10 +0100 blanchet no need for a script/mega-hack with the new SPASS
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing
Sun, 05 Feb 2012 12:27:10 +0100 blanchet tuning
Sun, 05 Feb 2012 11:14:25 +0100 bulwahn merged
Sun, 05 Feb 2012 10:43:52 +0100 bulwahn adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
Sun, 05 Feb 2012 10:42:57 +0100 bulwahn tuning to remove ML warnings
Sun, 05 Feb 2012 10:50:34 +0100 blanchet removed double filtering of type args
Sun, 05 Feb 2012 08:57:03 +0100 bulwahn adding a quickcheck example about functions and sets
Sun, 05 Feb 2012 08:47:13 +0100 bulwahn removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
Sun, 05 Feb 2012 08:36:41 +0100 bulwahn adding a remark about lemma which is too special and should be removed
Sun, 05 Feb 2012 08:24:39 +0100 bulwahn another try to improve code generation of set equality (cf. da32cf32c0c7)
Sun, 05 Feb 2012 08:24:38 +0100 bulwahn beautifying definitions of check_all and adding instance for finite_4
Sun, 05 Feb 2012 07:05:34 +0100 Cezary Kaliszyk Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Sat, 04 Feb 2012 17:01:25 +0100 blanchet added option to Mirabelle/Sledgehammer
Sat, 04 Feb 2012 12:08:18 +0100 blanchet improved hashing w.r.t. Mirabelle, to help debugging
Sat, 04 Feb 2012 12:08:18 +0100 blanchet tuned SPASS DFG output
Sat, 04 Feb 2012 12:08:18 +0100 blanchet the new SPASS gives accurate fact information, so no need for old hack anymore
Sat, 04 Feb 2012 12:08:18 +0100 blanchet fixed docs
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made sure to filter type args also for "uncurried alias" equations
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip