Wed, 15 Feb 2012 19:31:27 +0100 wenzelm NEWS;
Wed, 15 Feb 2012 17:49:03 +0100 wenzelm updated refs;
Wed, 15 Feb 2012 13:24:22 +0100 wenzelm renamed "xstr" to "str_token";
Tue, 14 Feb 2012 22:48:07 +0100 wenzelm merged
Tue, 14 Feb 2012 20:13:07 +0100 blanchet don't report spurious LEO-II errors
Tue, 14 Feb 2012 18:58:33 +0100 blanchet better error message
Tue, 14 Feb 2012 17:59:10 +0100 bulwahn removing debug code in mutabelle
Tue, 14 Feb 2012 17:58:51 +0100 bulwahn adding abort_potential functionality in quickcheck
Tue, 14 Feb 2012 17:29:53 +0100 bulwahn adding abort_potential configuration in Quickcheck
Tue, 14 Feb 2012 22:27:33 +0100 wenzelm clarified bires_inst_tac: retain internal exceptions;
Tue, 14 Feb 2012 22:22:01 +0100 wenzelm tuned signature;
Tue, 14 Feb 2012 21:59:10 +0100 wenzelm more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it;
Tue, 14 Feb 2012 21:45:32 +0100 wenzelm more conventional tactic setup;
Tue, 14 Feb 2012 21:31:26 +0100 wenzelm eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
Tue, 14 Feb 2012 21:19:39 +0100 wenzelm prefer high-level elim_format;
Tue, 14 Feb 2012 20:57:05 +0100 wenzelm discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip