Tue, 27 Apr 2010 08:17:39 +0200 haftmann canonical import
Mon, 26 Apr 2010 15:38:14 +0200 haftmann merged
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 23:46:45 +0200 blanchet merged
Mon, 26 Apr 2010 23:45:51 +0200 blanchet renamed option
Mon, 26 Apr 2010 23:45:32 +0200 blanchet fixes 2a5c6e7b55cb;
Mon, 26 Apr 2010 21:50:36 +0200 blanchet compile
Mon, 26 Apr 2010 21:41:54 +0200 blanchet make compile (and not just load dynamically)
Mon, 26 Apr 2010 21:25:32 +0200 blanchet merge
Mon, 26 Apr 2010 21:20:43 +0200 blanchet introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
Mon, 26 Apr 2010 21:18:20 +0200 blanchet adapt code to reflect new signature of "neg_clausify"
Mon, 26 Apr 2010 21:17:41 +0200 blanchet rename options and keep track of conjecture shape (to facilitate proof reconstruction)
Mon, 26 Apr 2010 21:17:04 +0200 blanchet rename options
Mon, 26 Apr 2010 21:16:35 +0200 blanchet make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
Mon, 26 Apr 2010 21:14:28 +0200 blanchet remove needless code that was copy-pasted from Quickcheck (where it made sense)
Sun, 25 Apr 2010 15:30:33 +0200 blanchet cosmetics
Sun, 25 Apr 2010 15:04:20 +0200 blanchet cosmetics
Sun, 25 Apr 2010 14:40:36 +0200 blanchet move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
Sun, 25 Apr 2010 11:38:46 +0200 blanchet support readable names even when Isar proof reconstruction is enabled -- useful for debugging
Sun, 25 Apr 2010 10:22:31 +0200 blanchet cosmetics: rename internal functions
Sun, 25 Apr 2010 00:33:26 +0200 blanchet cosmetics
Sun, 25 Apr 2010 00:25:44 +0200 blanchet remove "show_skolems" option and change style of record declarations
Sun, 25 Apr 2010 00:10:30 +0200 blanchet remove "skolemize" option from Nitpick, since Skolemization is always useful
Sat, 24 Apr 2010 17:48:21 +0200 blanchet removed Nitpick's "uncurry" option
Sat, 24 Apr 2010 16:44:45 +0200 blanchet fix typesetting
Sat, 24 Apr 2010 16:43:03 +0200 blanchet Fruhjahrsputz: remove three mostly useless Nitpick options
Sat, 24 Apr 2010 16:33:01 +0200 blanchet remove type annotations as comments;
Sat, 24 Apr 2010 16:17:30 +0200 blanchet cosmetics
Sat, 24 Apr 2010 16:05:42 +0200 blanchet better error reporting;
Fri, 23 Apr 2010 19:36:49 +0200 blanchet cosmetics
Fri, 23 Apr 2010 19:26:39 +0200 blanchet reuse timestamp function
Fri, 23 Apr 2010 19:18:39 +0200 blanchet stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
Fri, 23 Apr 2010 19:16:52 +0200 blanchet make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
Fri, 23 Apr 2010 19:12:49 +0200 blanchet remove some bloat
Fri, 23 Apr 2010 18:11:41 +0200 blanchet now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
Fri, 23 Apr 2010 18:06:41 +0200 blanchet renamed module "ATP_Wrapper" to "ATP_Systems"
Fri, 23 Apr 2010 17:38:25 +0200 blanchet move the minimizer to the Sledgehammer directory
Fri, 23 Apr 2010 16:59:48 +0200 blanchet remove debugging code
Fri, 23 Apr 2010 16:55:51 +0200 blanchet move some sledgehammer stuff out of "atp_manager.ML"
Fri, 23 Apr 2010 16:21:47 +0200 blanchet give an error if no ATP is set
Fri, 23 Apr 2010 16:15:35 +0200 blanchet move the Sledgehammer menu options to "sledgehammer_isar.ML"
Fri, 23 Apr 2010 15:48:34 +0200 blanchet centralized ATP-specific error handling in "atp_wrapper.ML"
Fri, 23 Apr 2010 13:16:50 +0200 blanchet handle ATP proof delimiters in a cleaner, more extensible fashion
Mon, 26 Apr 2010 22:59:28 +0200 wenzelm merged
Mon, 26 Apr 2010 11:08:49 -0700 huffman fix another if-then-else parse error
Mon, 26 Apr 2010 10:57:04 -0700 huffman fix if-then-else parse error
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:37:46 -0700 huffman fix syntax precedence declarations for UNION, INTER, SUP, INF
Mon, 26 Apr 2010 09:26:31 -0700 huffman syntax precedence for If and Let
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Sun, 25 Apr 2010 23:22:29 -0700 huffman fix duplicate simp rule warnings
Sun, 25 Apr 2010 20:48:19 -0700 huffman define finer-than ordering on net type; move some theorems into Limits.thy
Sun, 25 Apr 2010 16:23:40 -0700 huffman generalize type of continuous_on
Sun, 25 Apr 2010 11:58:39 -0700 huffman define nets directly as filters, instead of as filter bases
Mon, 26 Apr 2010 21:50:28 +0200 wenzelm use 'example_proof' (invisible);
Mon, 26 Apr 2010 21:45:08 +0200 wenzelm command 'example_proof' opens an empty proof body;
Mon, 26 Apr 2010 21:36:44 +0200 wenzelm proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;
Mon, 26 Apr 2010 20:30:50 +0200 wenzelm eliminanated some unreferenced identifiers;
Mon, 26 Apr 2010 16:08:04 +0200 wenzelm merged
Mon, 26 Apr 2010 15:14:14 +0200 Cezary Kaliszyk add bounded_lattice_bot and bounded_lattice_top type classes
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip