haftmann [Tue, 21 Dec 2010 15:16:27 +0100] rev 41366
merged
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