| 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
|
| Mon, 20 Dec 2010 18:48:13 +0100 |
blanchet |
merged
|
changeset |
files
|
| Mon, 20 Dec 2010 14:55:24 +0100 |
blanchet |
run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
|
changeset |
files
|
| Mon, 20 Dec 2010 14:17:49 +0100 |
blanchet |
disable feature that was enabled by mistake
|
changeset |
files
|
| Mon, 20 Dec 2010 14:10:40 +0100 |
blanchet |
make exceptions more transparent in "debug" mode
|
changeset |
files
|
| Mon, 20 Dec 2010 14:09:45 +0100 |
blanchet |
remove spurious line
|
changeset |
files
|
| Mon, 20 Dec 2010 13:52:44 +0100 |
blanchet |
use the options provided by Stephan Schulz -- much better
|
changeset |
files
|
| Mon, 20 Dec 2010 12:12:35 +0100 |
blanchet |
optionally supply constant weights to E -- turned off by default until properly parameterized
|
changeset |
files
|
| Mon, 20 Dec 2010 17:31:58 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 20 Dec 2010 15:37:25 +0100 |
haftmann |
type_lifting for predicates
|
changeset |
files
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
changeset |
files
|
| Mon, 20 Dec 2010 15:24:25 +0100 |
wenzelm |
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
|
changeset |
files
|
| Mon, 20 Dec 2010 15:19:15 +0100 |
wenzelm |
tuned/clarified some component settings;
|
changeset |
files
|
| Mon, 20 Dec 2010 14:44:00 +0100 |
wenzelm |
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
|
changeset |
files
|
| Mon, 20 Dec 2010 13:36:25 +0100 |
wenzelm |
purged some comments (Locale_Test is already clean thanks to configuration options);
|
changeset |
files
|
| Mon, 20 Dec 2010 13:24:04 +0100 |
wenzelm |
actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;
|
changeset |
files
|
| Mon, 20 Dec 2010 09:45:26 +0100 |
boehmes |
merged
|
changeset |
files
|
| Mon, 20 Dec 2010 09:31:47 +0100 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Mon, 20 Dec 2010 09:06:37 +0100 |
boehmes |
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
|
changeset |
files
|
| Mon, 20 Dec 2010 08:45:27 +0100 |
boehmes |
derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
|
changeset |
files
|
| Mon, 20 Dec 2010 08:17:23 +0100 |
boehmes |
perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
|
changeset |
files
|
| Mon, 20 Dec 2010 08:55:36 +0100 |
haftmann |
merge
|
changeset |
files
|
| Fri, 17 Dec 2010 22:00:54 +0100 |
haftmann |
more convenient order of type variables
|
changeset |
files
|
| Sun, 19 Dec 2010 18:38:50 -0800 |
huffman |
rename function cprod_map to prod_map
|
changeset |
files
|
| Sun, 19 Dec 2010 18:15:21 -0800 |
huffman |
switch to transparent ascription, to avoid warning messages
|
changeset |
files
|
| Sun, 19 Dec 2010 18:11:20 -0800 |
huffman |
types -> type_synonym
|
changeset |
files
|
| Sun, 19 Dec 2010 18:10:54 -0800 |
huffman |
fix typo
|
changeset |
files
|
| Sun, 19 Dec 2010 17:39:20 -0800 |
huffman |
merged
|
changeset |
files
|