| Tue, 21 Dec 2010 21:54:51 +0100 |
wenzelm |
configuration option "rule_trace";
|
changeset |
files
|
| Tue, 21 Dec 2010 21:31:36 +0100 |
wenzelm |
configuration option "syntax_branching_level";
|
changeset |
files
|
| Tue, 21 Dec 2010 21:21:21 +0100 |
wenzelm |
configuration option "syntax_ast_trace" and "syntax_ast_stat";
|
changeset |
files
|
| Tue, 21 Dec 2010 21:05:50 +0100 |
wenzelm |
more robust ML antiquotations -- allow original tokens without adjacent whitespace;
|
changeset |
files
|
| Tue, 21 Dec 2010 19:35:36 +0100 |
wenzelm |
configuration option "ML_trace";
|
changeset |
files
|
| Tue, 21 Dec 2010 17:52:35 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
id_const replaces mk_id
|
changeset |
files
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
changeset |
files
|
| Tue, 21 Dec 2010 16:14:46 +0100 |
haftmann |
prove more algebraic version of functorial properties; retain old properties for convenience
|
changeset |
files
|
| Tue, 21 Dec 2010 08:43:39 -0800 |
huffman |
declare more simp rules, rewrite proofs in Isar-style
|
changeset |
files
|
| Tue, 21 Dec 2010 16:41:31 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 15:00:59 +0100 |
hoelzl |
use DERIV_intros
|
changeset |
files
|
| Tue, 21 Dec 2010 14:50:53 +0100 |
hoelzl |
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
|
changeset |
files
|
| Tue, 21 Dec 2010 15:16:27 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 15:15:55 +0100 |
haftmann |
proper static closures
|
changeset |
files
|
| Tue, 21 Dec 2010 15:15:55 +0100 |
haftmann |
tuned names
|
changeset |
files
|
| Tue, 21 Dec 2010 14:54:23 +0100 |
haftmann |
renamed mk_id to the more canonical id_const
|
changeset |
files
|
| Tue, 21 Dec 2010 14:18:45 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 13:57:35 +0100 |
blanchet |
better parsing of options, in case the value has '='
|
changeset |
files
|
| Tue, 21 Dec 2010 13:57:19 +0100 |
blanchet |
show the relation
|
changeset |
files
|
| Tue, 21 Dec 2010 10:25:17 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 10:24:56 +0100 |
blanchet |
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
|
changeset |
files
|
| Tue, 21 Dec 2010 10:18:56 +0100 |
blanchet |
added "sledgehammer_tac" as possible reconstructor in Mirabelle
|
changeset |
files
|
| Tue, 21 Dec 2010 12:48:47 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 12:02:05 +0100 |
boehmes |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 11:05:30 +0100 |
boehmes |
also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
|
changeset |
files
|
| Tue, 21 Dec 2010 01:12:14 +0100 |
traytel |
Enabled non fully polymorphic map functions in subtyping
|
changeset |
files
|
| Tue, 21 Dec 2010 11:54:35 +0100 |
wenzelm |
make SML/NJ and Poly/ML agree on the type of "before";
|
changeset |
files
|
| Tue, 21 Dec 2010 10:20:33 +0100 |
haftmann |
only depend on exisiting statements
|
changeset |
files
|
| Tue, 21 Dec 2010 09:29:53 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 09:29:33 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 09:19:37 +0100 |
haftmann |
tuned naming
|
changeset |
files
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
canonical handling of theory context argument
|
changeset |
files
|
| Tue, 21 Dec 2010 09:16:03 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
evaluator separating static and dynamic operations
|
changeset |
files
|
| Tue, 21 Dec 2010 08:40:39 +0100 |
haftmann |
program is separate argument to serializer
|
changeset |
files
|
| Tue, 21 Dec 2010 07:45:04 +0100 |
haftmann |
more explicit structure for serializer invocation
|
changeset |
files
|
| Tue, 21 Dec 2010 08:38:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Tue, 21 Dec 2010 08:37:48 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| Tue, 21 Dec 2010 07:23:21 +0100 |
haftmann |
HOLogic.mk_id
|
changeset |
files
|
| Tue, 21 Dec 2010 06:53:20 +0100 |
blanchet |
avoid weird symbols in path
|
changeset |
files
|
| Tue, 21 Dec 2010 06:06:28 +0100 |
blanchet |
mechanism to keep SMT input and output files around in Mirabelle
|
changeset |
files
|
| Tue, 21 Dec 2010 04:33:17 +0100 |
blanchet |
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
|
changeset |
files
|
| Tue, 21 Dec 2010 03:56:51 +0100 |
blanchet |
added "smt_triggers" option to experiment with triggers in Sledgehammer;
|
changeset |
files
|
| Tue, 21 Dec 2010 01:12:17 +0100 |
blanchet |
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
|
changeset |
files
|
| Mon, 20 Dec 2010 23:36:58 +0100 |
wenzelm |
Cygwin: Poly/ML 5.4.0 requires libgmp3;
|
changeset |
files
|
| Mon, 20 Dec 2010 23:30:32 +0100 |
wenzelm |
updated to polyml-5.4.0;
|
changeset |
files
|
| Mon, 20 Dec 2010 23:26:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 20 Dec 2010 23:19:16 +0100 |
wenzelm |
updated for Poly/ML 5.4.0;
|
changeset |
files
|
| Mon, 20 Dec 2010 22:27:26 +0100 |
boehmes |
merged
|
changeset |
files
|
| Mon, 20 Dec 2010 22:02:57 +0100 |
boehmes |
avoid ML structure aliases (especially single-letter abbreviations)
|
changeset |
files
|
| Mon, 20 Dec 2010 21:04:45 +0100 |
boehmes |
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
|
changeset |
files
|
| Mon, 20 Dec 2010 11:11:51 -0800 |
huffman |
merged
|
changeset |
files
|
| Mon, 20 Dec 2010 10:57:01 -0800 |
huffman |
configure domain package to work with HOL option type
|
changeset |
files
|
| Mon, 20 Dec 2010 10:48:01 -0800 |
huffman |
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
|
changeset |
files
|
| Mon, 20 Dec 2010 09:48:16 -0800 |
huffman |
simplify proofs
|
changeset |
files
|
| Mon, 20 Dec 2010 09:41:55 -0800 |
huffman |
beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
|
changeset |
files
|
| Mon, 20 Dec 2010 08:26:47 -0800 |
huffman |
configure domain package to work with HOL sum type
|
changeset |
files
|
| Mon, 20 Dec 2010 07:50:47 -0800 |
huffman |
replace list_map function with an abbreviation
|
changeset |
files
|