haftmann [Tue, 21 Dec 2010 15:15:55 +0100] rev 41365
proper static closures
haftmann [Tue, 21 Dec 2010 15:15:55 +0100] rev 41364
tuned names
haftmann [Tue, 21 Dec 2010 14:54:23 +0100] rev 41363
renamed mk_id to the more canonical id_const
blanchet [Tue, 21 Dec 2010 14:18:45 +0100] rev 41362
merged
blanchet [Tue, 21 Dec 2010 13:57:35 +0100] rev 41361
better parsing of options, in case the value has '='
blanchet [Tue, 21 Dec 2010 13:57:19 +0100] rev 41360
show the relation
blanchet [Tue, 21 Dec 2010 10:25:17 +0100] rev 41359
merged
blanchet [Tue, 21 Dec 2010 10:24:56 +0100] rev 41358
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
use it in "Mirabelle.thy"
blanchet [Tue, 21 Dec 2010 10:18:56 +0100] rev 41357
added "sledgehammer_tac" as possible reconstructor in Mirabelle
wenzelm [Tue, 21 Dec 2010 12:48:47 +0100] rev 41356
merged
boehmes [Tue, 21 Dec 2010 12:02:05 +0100] rev 41355
merged
boehmes [Tue, 21 Dec 2010 11:05:30 +0100] rev 41354
also provide a view on arguments for "external" built-in symbols (similar to "internal" (real) built-in symbols)
traytel [Tue, 21 Dec 2010 01:12:14 +0100] rev 41353
Enabled non fully polymorphic map functions in subtyping
wenzelm [Tue, 21 Dec 2010 11:54:35 +0100] rev 41352
make SML/NJ and Poly/ML agree on the type of "before";
haftmann [Tue, 21 Dec 2010 10:20:33 +0100] rev 41351
only depend on exisiting statements
haftmann [Tue, 21 Dec 2010 09:29:53 +0100] rev 41350
merged
haftmann [Tue, 21 Dec 2010 09:29:33 +0100] rev 41349
evaluator separating static and dynamic operations
haftmann [Tue, 21 Dec 2010 09:19:37 +0100] rev 41348
tuned naming
haftmann [Tue, 21 Dec 2010 09:18:29 +0100] rev 41347
evaluator separating static and dynamic operations
haftmann [Tue, 21 Dec 2010 09:18:29 +0100] rev 41346
canonical handling of theory context argument
haftmann [Tue, 21 Dec 2010 09:16:03 +0100] rev 41345
merged
haftmann [Tue, 21 Dec 2010 08:40:39 +0100] rev 41344
evaluator separating static and dynamic operations
haftmann [Tue, 21 Dec 2010 08:40:39 +0100] rev 41343
program is separate argument to serializer
haftmann [Tue, 21 Dec 2010 07:45:04 +0100] rev 41342
more explicit structure for serializer invocation
nipkow [Tue, 21 Dec 2010 08:38:03 +0100] rev 41341
merged
nipkow [Tue, 21 Dec 2010 08:37:48 +0100] rev 41340
tuned proof
haftmann [Tue, 21 Dec 2010 07:23:21 +0100] rev 41339
HOLogic.mk_id
blanchet [Tue, 21 Dec 2010 06:53:20 +0100] rev 41338
avoid weird symbols in path
blanchet [Tue, 21 Dec 2010 06:06:28 +0100] rev 41337
mechanism to keep SMT input and output files around in Mirabelle
blanchet [Tue, 21 Dec 2010 04:33:17 +0100] rev 41336
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
blanchet [Tue, 21 Dec 2010 03:56:51 +0100] rev 41335
added "smt_triggers" option to experiment with triggers in Sledgehammer;
renamings (for consistency)
blanchet [Tue, 21 Dec 2010 01:12:17 +0100] rev 41334
enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
wenzelm [Mon, 20 Dec 2010 23:36:58 +0100] rev 41333
Cygwin: Poly/ML 5.4.0 requires libgmp3;
wenzelm [Mon, 20 Dec 2010 23:30:32 +0100] rev 41332
updated to polyml-5.4.0;
wenzelm [Mon, 20 Dec 2010 23:26:17 +0100] rev 41331
tuned;
wenzelm [Mon, 20 Dec 2010 23:19:16 +0100] rev 41330
updated for Poly/ML 5.4.0;
boehmes [Mon, 20 Dec 2010 22:27:26 +0100] rev 41329
merged
boehmes [Mon, 20 Dec 2010 22:02:57 +0100] rev 41328
avoid ML structure aliases (especially single-letter abbreviations)
boehmes [Mon, 20 Dec 2010 21:04:45 +0100] rev 41327
added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
huffman [Mon, 20 Dec 2010 11:11:51 -0800] rev 41326
merged
huffman [Mon, 20 Dec 2010 10:57:01 -0800] rev 41325
configure domain package to work with HOL option type
huffman [Mon, 20 Dec 2010 10:48:01 -0800] rev 41324
make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman [Mon, 20 Dec 2010 09:48:16 -0800] rev 41323
simplify proofs
huffman [Mon, 20 Dec 2010 09:41:55 -0800] rev 41322
beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
huffman [Mon, 20 Dec 2010 08:26:47 -0800] rev 41321
configure domain package to work with HOL sum type
huffman [Mon, 20 Dec 2010 07:50:47 -0800] rev 41320
replace list_map function with an abbreviation
blanchet [Mon, 20 Dec 2010 18:48:13 +0100] rev 41319
merged
blanchet [Mon, 20 Dec 2010 14:55:24 +0100] rev 41318
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
blanchet [Mon, 20 Dec 2010 14:17:49 +0100] rev 41317
disable feature that was enabled by mistake
blanchet [Mon, 20 Dec 2010 14:10:40 +0100] rev 41316
make exceptions more transparent in "debug" mode
blanchet [Mon, 20 Dec 2010 14:09:45 +0100] rev 41315
remove spurious line
blanchet [Mon, 20 Dec 2010 13:52:44 +0100] rev 41314
use the options provided by Stephan Schulz -- much better
blanchet [Mon, 20 Dec 2010 12:12:35 +0100] rev 41313
optionally supply constant weights to E -- turned off by default until properly parameterized
haftmann [Mon, 20 Dec 2010 17:31:58 +0100] rev 41312
merged
haftmann [Mon, 20 Dec 2010 15:37:25 +0100] rev 41311
type_lifting for predicates
wenzelm [Mon, 20 Dec 2010 16:44:33 +0100] rev 41310
proper identifiers for consts and types;
wenzelm [Mon, 20 Dec 2010 15:24:25 +0100] rev 41309
some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
wenzelm [Mon, 20 Dec 2010 15:19:15 +0100] rev 41308
tuned/clarified some component settings;
explicit comments about common mistakes;
wenzelm [Mon, 20 Dec 2010 14:44:00 +0100] rev 41307
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;
wenzelm [Mon, 20 Dec 2010 13:36:25 +0100] rev 41306
purged some comments (Locale_Test is already clean thanks to configuration options);