Thu, 29 Apr 2010 17:50:11 +0200 wenzelm merged
Thu, 29 Apr 2010 09:06:35 +0200 Cezary Kaliszyk Tuning the quotient examples
Wed, 28 Apr 2010 17:42:37 +0200 krauss clarified signature; simpler implementation in terms of function's tactic interface
Wed, 28 Apr 2010 16:13:17 +0200 krauss return info record (relative to auxiliary context!)
Wed, 28 Apr 2010 11:52:04 +0200 krauss default termination prover as plain tactic
Wed, 28 Apr 2010 10:31:15 +0200 krauss function: sane interface for programmatic use
Wed, 28 Apr 2010 09:48:22 +0200 krauss ML interface uses plain command names, following conventions from typedef
Wed, 28 Apr 2010 09:21:48 +0200 krauss function: better separate Isar integration from actual functionality
Thu, 29 Apr 2010 07:02:22 +0200 haftmann merged
Wed, 28 Apr 2010 17:04:56 +0200 haftmann export somehow odd mapa explicitly
Wed, 28 Apr 2010 16:56:19 +0200 haftmann exported print_tuple
Wed, 28 Apr 2010 16:56:18 +0200 haftmann take into account tupled constructors
Wed, 28 Apr 2010 16:56:18 +0200 haftmann avoid code_datatype antiquotation
Wed, 28 Apr 2010 19:46:09 +0200 bulwahn merged
Wed, 28 Apr 2010 16:45:51 +0200 bulwahn added an example with a free function variable to the Predicate Compile examples
Wed, 28 Apr 2010 16:45:50 +0200 bulwahn removed local clone in the predicate compiler
Wed, 28 Apr 2010 16:45:48 +0200 bulwahn improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
Thu, 29 Apr 2010 17:47:53 +0200 wenzelm allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
Thu, 29 Apr 2010 17:29:53 +0200 wenzelm 'write': actually observe the proof structure (like 'let' or 'fix');
Thu, 29 Apr 2010 17:15:23 +0200 wenzelm adapted ProofContext.infer_type;
Thu, 29 Apr 2010 16:55:22 +0200 wenzelm ProofContext.read_const: allow for type constraint (for fixed variable);
Thu, 29 Apr 2010 16:53:08 +0200 wenzelm avoid clash with keyword 'write';
Thu, 29 Apr 2010 11:05:13 +0200 wenzelm allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
Thu, 29 Apr 2010 11:00:32 +0200 wenzelm uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
Wed, 28 Apr 2010 19:43:45 +0200 wenzelm disabled spurious invocation of (interactive) sledgehammer;
Wed, 28 Apr 2010 17:29:58 +0200 wenzelm merged
Wed, 28 Apr 2010 16:56:03 +0200 blanchet make Mirabelle happy
Wed, 28 Apr 2010 16:47:56 +0200 blanchet remove removed option
Wed, 28 Apr 2010 16:15:45 +0200 blanchet merge
Wed, 28 Apr 2010 16:14:56 +0200 blanchet parentheses around nested cases
Wed, 28 Apr 2010 16:06:27 +0200 blanchet merged
Wed, 28 Apr 2010 16:05:38 +0200 blanchet add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
Wed, 28 Apr 2010 16:03:49 +0200 blanchet reintroduced short names for HOL->FOL constants; other parts of the code rely on these
Wed, 28 Apr 2010 15:53:17 +0200 blanchet save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
Wed, 28 Apr 2010 15:34:55 +0200 blanchet unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
Wed, 28 Apr 2010 14:19:26 +0200 blanchet redo Sledgehammer proofs (and get rid of "neg_clausify")
Wed, 28 Apr 2010 13:32:45 +0200 blanchet removed "sorts" option, continued
Wed, 28 Apr 2010 13:00:30 +0200 blanchet remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
Wed, 28 Apr 2010 12:49:52 +0200 blanchet insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
Wed, 28 Apr 2010 12:46:50 +0200 blanchet support Vampire definitions of constants as "let" constructs in Isar proofs
Tue, 27 Apr 2010 18:58:05 +0200 blanchet tuning
Tue, 27 Apr 2010 18:07:51 +0200 blanchet redid the proofs with the latest Sledgehammer;
Tue, 27 Apr 2010 18:02:46 +0200 blanchet remove Nitpick functions that are now implemented in Sledgehammer
Tue, 27 Apr 2010 18:01:41 +0200 blanchet added total goal count as argument + message when killing ATPs
Tue, 27 Apr 2010 17:44:33 +0200 blanchet make Sledgehammer more friendly if no subgoal is left
Tue, 27 Apr 2010 17:05:39 +0200 blanchet polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs
Tue, 27 Apr 2010 16:12:51 +0200 blanchet reintroduce missing "gen_all_vars" call
Tue, 27 Apr 2010 16:00:20 +0200 blanchet fix types of "fix" variables to help proof reconstruction and aid readability
Tue, 27 Apr 2010 14:55:10 +0200 blanchet allow schematic variables in types in terms that are reconstructed by Sledgehammer
Tue, 27 Apr 2010 14:27:47 +0200 blanchet in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
Tue, 27 Apr 2010 12:07:07 +0200 blanchet new Isar proof construction code: stringfy axiom names correctly
Tue, 27 Apr 2010 11:44:01 +0200 blanchet honor "shrink_proof" Sledgehammer option
Tue, 27 Apr 2010 11:24:47 +0200 blanchet remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
Wed, 28 Apr 2010 15:42:10 +0200 haftmann updated keywords
Wed, 28 Apr 2010 15:17:13 +0200 haftmann exported cert_tyco, read_tyco
Wed, 28 Apr 2010 15:17:09 +0200 haftmann added code_reflect command
Wed, 28 Apr 2010 14:54:17 +0200 haftmann merged
Wed, 28 Apr 2010 11:26:10 +0200 haftmann fix "fors" for proof of monotonicity
Wed, 28 Apr 2010 14:01:54 +0200 Cezary Kaliszyk merge
Wed, 28 Apr 2010 14:01:13 +0200 Cezary Kaliszyk merge
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip