Sat, 01 Feb 2014 18:22:38 +0100 wenzelm method_setup "lem";
Sat, 01 Feb 2014 18:17:13 +0100 wenzelm lazy_pack is default context for ILL;
Sat, 01 Feb 2014 18:07:10 +0100 wenzelm unused;
Sat, 01 Feb 2014 18:05:03 +0100 wenzelm proper Simplifier method setup;
Sat, 01 Feb 2014 18:00:28 +0100 wenzelm simplified sessions;
Sat, 01 Feb 2014 17:56:03 +0100 wenzelm misc tuning and modernization;
Sat, 01 Feb 2014 00:32:32 +0000 paulson version of Fermat's Theorem for type nat
Fri, 31 Jan 2014 19:32:13 +0100 wenzelm merged
Fri, 31 Jan 2014 18:58:50 +0100 wenzelm merged
Fri, 31 Jan 2014 17:35:19 +0100 wenzelm include comment.sty 3.6 which still works with plain tex, in contrast to later 3.7 which is only for latex (slow due to file snippets) -- see also 30781cc78fc6;
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added a 'trace' option
Fri, 31 Jan 2014 18:43:16 +0100 blanchet tuning
Fri, 31 Jan 2014 18:43:16 +0100 blanchet moved code around
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added 'algebra' to the mix
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more informative trace
Fri, 31 Jan 2014 18:43:16 +0100 blanchet tuning
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more concise Isar output
Fri, 31 Jan 2014 16:58:58 +0000 paulson Restoring some proofs from the equivalent file in Old_Number_Theory.
Fri, 31 Jan 2014 16:41:54 +0100 blanchet better tracing + syntactically correct 'metis' calls
Fri, 31 Jan 2014 16:26:43 +0100 blanchet tuned ML function names
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Fri, 31 Jan 2014 16:07:20 +0100 blanchet moved ML code around
Fri, 31 Jan 2014 14:33:02 +0100 wenzelm tuned headers;
Fri, 31 Jan 2014 13:45:39 +0100 blanchet merge
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip