Fri, 31 Jan 2014 13:42:47 +0100 blanchet compile
Fri, 31 Jan 2014 13:32:13 +0100 blanchet guarded against exception
Fri, 31 Jan 2014 13:29:20 +0100 blanchet tuning
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file
Fri, 31 Jan 2014 12:16:59 +0100 traytel use Local_Theory.define instead of Specification.definition for internal constants
Fri, 31 Jan 2014 10:34:20 +0100 blanchet compile
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned comment
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name
Fri, 31 Jan 2014 10:02:36 +0100 traytel less hermetic tactics
Thu, 30 Jan 2014 22:55:52 +0100 blanchet merged
Thu, 30 Jan 2014 22:42:29 +0100 blanchet reverted unsound optimization
Thu, 30 Jan 2014 21:56:25 +0100 blanchet got rid of one of two Metis variants
Thu, 30 Jan 2014 21:02:19 +0100 blanchet tuning
Thu, 30 Jan 2014 20:39:49 +0100 blanchet unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
Thu, 30 Jan 2014 18:37:08 +0100 blanchet killed needless pass
Thu, 30 Jan 2014 16:30:01 +0100 haftmann dependency reporting for code generation errors
Thu, 30 Jan 2014 16:30:00 +0100 haftmann more abstract dictionary construction
Thu, 30 Jan 2014 16:09:04 +0100 haftmann reduced prominence of "permissive code generation"
Thu, 30 Jan 2014 16:09:03 +0100 haftmann split rules for of_bool, similar to if
Thu, 30 Jan 2014 17:34:42 +0100 blanchet don't forget the last inference(s) after conjecture skolemization
Thu, 30 Jan 2014 16:40:31 +0100 blanchet centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
Thu, 30 Jan 2014 15:01:40 +0100 blanchet keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions
Thu, 30 Jan 2014 14:28:04 +0100 blanchet more robust w.r.t. exceptions raised by proof methods
Thu, 30 Jan 2014 14:24:10 +0100 blanchet tuning
Thu, 30 Jan 2014 13:54:12 +0100 blanchet compile
Thu, 30 Jan 2014 13:39:57 +0100 blanchet tuning
Thu, 30 Jan 2014 13:38:28 +0100 blanchet added 'algebra' and 'meson' to 'try0'
Thu, 30 Jan 2014 13:38:28 +0100 blanchet made 'try0' (more) silent
Thu, 30 Jan 2014 13:38:28 +0100 blanchet 'using' already uses the new Skolemizer, enabling a subtly shorter syntax
Thu, 30 Jan 2014 13:31:56 +0100 traytel merged
Thu, 30 Jan 2014 12:28:05 +0100 traytel extended cardinals library
Thu, 30 Jan 2014 12:27:42 +0100 traytel define ofilter outside of wo_rel
Thu, 30 Jan 2014 10:00:53 +0100 haftmann more direct simplification rules for 1 div/mod numeral;
Thu, 30 Jan 2014 01:03:55 +0100 blanchet systematically suppress tracing if asked for (affects 'meson' proof method)
Thu, 30 Jan 2014 00:59:12 +0100 blanchet silenced reconstructors in Sledgehammer
Wed, 29 Jan 2014 23:24:34 +0100 blanchet proper 'show' detection
Wed, 29 Jan 2014 22:34:34 +0100 blanchet correctly handle exceptions arising from (experimental) Isar proof code
Wed, 29 Jan 2014 20:11:38 +0100 haftmann made smlnj happy
Wed, 29 Jan 2014 17:09:46 +0000 paulson Merge
Wed, 29 Jan 2014 17:09:01 +0000 paulson Removed a dependence upon Old_Number_Theory. Simplified a few proofs.
Wed, 29 Jan 2014 16:47:06 +0100 traytel merged
Wed, 29 Jan 2014 16:35:05 +0100 traytel made tactic more robust
Wed, 29 Jan 2014 15:41:18 +0000 paulson Merge
Wed, 29 Jan 2014 15:40:33 +0000 paulson minor adjustments
Wed, 29 Jan 2014 15:05:53 +0100 blanchet added Dmitriy, since he did the case syntax
Wed, 29 Jan 2014 12:51:37 +0000 paulson Replacing the theory Library/Binomial by Number_Theory/Binomial
Mon, 27 Jan 2014 17:13:33 +0000 paulson Merge
Mon, 27 Jan 2014 16:38:52 +0000 paulson converting to new Number_Theory
Mon, 27 Jan 2014 12:16:08 +0100 wenzelm tuned;
Mon, 27 Jan 2014 12:10:00 +0100 wenzelm tuned signature;
Sun, 26 Jan 2014 16:23:47 +0100 haftmann obsolete
Sun, 26 Jan 2014 16:23:46 +0100 haftmann more suitable names, without any notion of "activating"
Sun, 26 Jan 2014 14:01:19 +0100 wenzelm discontinued obsolete attribute "standard";
Sun, 26 Jan 2014 13:45:40 +0100 wenzelm tuned signature;
Sat, 25 Jan 2014 23:50:49 +0100 haftmann less clumsy namespace
Sat, 25 Jan 2014 23:50:49 +0100 haftmann immediate "activation" of const syntax at declaration time
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip