blanchet [Fri, 01 Jul 2011 17:44:04 +0200] rev 43631
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
blanchet [Fri, 01 Jul 2011 16:31:33 +0200] rev 43630
made minimizer informative output accurate
blanchet [Fri, 01 Jul 2011 15:53:38 +0200] rev 43629
test a few more type encodings
blanchet [Fri, 01 Jul 2011 15:53:38 +0200] rev 43628
further repair "mangled_tags", now that tags are also mangled
blanchet [Fri, 01 Jul 2011 15:53:38 +0200] rev 43627
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
blanchet [Fri, 01 Jul 2011 15:53:38 +0200] rev 43626
renamed "type_sys" to "type_enc", which is more accurate
blanchet [Fri, 01 Jul 2011 15:53:37 +0200] rev 43625
document "simple_higher" type encoding
blanchet [Fri, 01 Jul 2011 15:53:37 +0200] rev 43624
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet [Fri, 01 Jul 2011 15:53:37 +0200] rev 43623
mangle "ti" tags
blanchet [Fri, 01 Jul 2011 15:53:37 +0200] rev 43622
tuning
wenzelm [Fri, 01 Jul 2011 17:36:25 +0200] rev 43621
clarified Thy_Syntax.element;
wenzelm [Fri, 01 Jul 2011 16:05:38 +0200] rev 43620
tuned layout;
wenzelm [Fri, 01 Jul 2011 15:16:03 +0200] rev 43619
proper @{binding} antiquotations (relevant for formal references);
wenzelm [Fri, 01 Jul 2011 15:14:44 +0200] rev 43618
tuned;
wenzelm [Fri, 01 Jul 2011 14:17:02 +0200] rev 43617
merged
noschinl [Fri, 01 Jul 2011 13:54:25 +0200] rev 43616
reverted 782991e4180d: fold_fields was never used
noschinl [Fri, 01 Jul 2011 13:54:23 +0200] rev 43615
reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
bulwahn [Fri, 01 Jul 2011 11:26:02 +0200] rev 43614
improving actual dependencies
bulwahn [Fri, 01 Jul 2011 10:45:51 +0200] rev 43613
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
bulwahn [Fri, 01 Jul 2011 10:45:49 +0200] rev 43612
adding a value antiquotation
wenzelm [Thu, 30 Jun 2011 19:24:09 +0200] rev 43611
more general theory header parsing;
wenzelm [Thu, 30 Jun 2011 16:50:26 +0200] rev 43610
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
wenzelm [Thu, 30 Jun 2011 16:07:30 +0200] rev 43609
merged
krauss [Thu, 30 Jun 2011 10:15:46 +0200] rev 43608
parse term in auxiliary context augmented with variable;
pass through binding appropriately;
more standard syntax and ML interface
boehmes [Wed, 29 Jun 2011 11:58:35 +0200] rev 43607
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)
wenzelm [Thu, 30 Jun 2011 14:55:01 +0200] rev 43606
prefer Isabelle path algebra;
wenzelm [Thu, 30 Jun 2011 14:51:32 +0200] rev 43605
proper fold order;
wenzelm [Thu, 30 Jun 2011 14:03:31 +0200] rev 43604
more Path operations;
tuned signature;
wenzelm [Thu, 30 Jun 2011 13:59:55 +0200] rev 43603
getenv_strict in ML;
tuned;
wenzelm [Thu, 30 Jun 2011 13:21:41 +0200] rev 43602
standardized use of Path operations;
wenzelm [Thu, 30 Jun 2011 11:15:36 +0200] rev 43601
tuned comments;
wenzelm [Thu, 30 Jun 2011 00:09:57 +0200] rev 43600
abstract algebra of file paths in Scala (cf. path.ML);
wenzelm [Thu, 30 Jun 2011 00:01:00 +0200] rev 43599
proper Path.print;
wenzelm [Wed, 29 Jun 2011 23:43:48 +0200] rev 43598
basic operations on lists and strings;
wenzelm [Wed, 29 Jun 2011 21:34:16 +0200] rev 43597
tuned signature;
wenzelm [Wed, 29 Jun 2011 20:39:41 +0200] rev 43596
simplified/unified Simplifier.mk_solver;
wenzelm [Wed, 29 Jun 2011 18:12:34 +0200] rev 43595
modernized some simproc setup;
wenzelm [Wed, 29 Jun 2011 17:35:46 +0200] rev 43594
modernized some simproc setup;
wenzelm [Wed, 29 Jun 2011 16:31:50 +0200] rev 43593
print Path.T with some markup;
wenzelm [Wed, 29 Jun 2011 15:23:36 +0200] rev 43592
HTML: render control symbols more like Isabelle/Scala/jEdit;
traytel [Tue, 28 Jun 2011 10:52:15 +0200] rev 43591
collapse map functions with identity subcoercions to identities;
blanchet [Tue, 28 Jun 2011 21:06:59 +0200] rev 43590
reenabled accidentally-disabled automatic minimization
wenzelm [Tue, 28 Jun 2011 20:42:29 +0200] rev 43589
tuned markup;
paulson [Tue, 28 Jun 2011 17:13:32 +0100] rev 43588
merged
paulson [Tue, 28 Jun 2011 17:12:50 +0100] rev 43587
tidied messy proofs
bulwahn [Tue, 28 Jun 2011 16:43:44 +0200] rev 43586
merged
bulwahn [Tue, 28 Jun 2011 14:36:43 +0200] rev 43585
adding timeout to quickcheck narrowing
paulson [Tue, 28 Jun 2011 14:52:46 +0100] rev 43584
simplified proofs using metis calls
paulson [Tue, 28 Jun 2011 12:48:00 +0100] rev 43583
merged
paulson [Tue, 28 Jun 2011 12:47:32 +0100] rev 43582
keyfree: The set of key-free messages (and associated theorems)
wenzelm [Mon, 27 Jun 2011 22:44:44 +0200] rev 43581
merged
krauss [Mon, 27 Jun 2011 17:04:04 +0200] rev 43580
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
renamed old version to info_of_constr_permissive, reflecting its semantics
blanchet [Mon, 27 Jun 2011 14:56:39 +0200] rev 43579
added reference for MESON
blanchet [Mon, 27 Jun 2011 14:56:37 +0200] rev 43578
document "meson" and "metis" in HOL specific section of the Isar ref manual
blanchet [Mon, 27 Jun 2011 14:56:35 +0200] rev 43577
clarify minimizer output
blanchet [Mon, 27 Jun 2011 14:56:33 +0200] rev 43576
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet [Mon, 27 Jun 2011 14:56:32 +0200] rev 43575
tweaked comment
blanchet [Mon, 27 Jun 2011 14:56:31 +0200] rev 43574
document "sound" option
blanchet [Mon, 27 Jun 2011 14:56:29 +0200] rev 43573
minor Sledgehammer news
blanchet [Mon, 27 Jun 2011 14:56:28 +0200] rev 43572
added "sound" option to force Sledgehammer to be pedantically sound
blanchet [Mon, 27 Jun 2011 14:56:26 +0200] rev 43571
removed "full_types" option from documentation
blanchet [Mon, 27 Jun 2011 14:56:10 +0200] rev 43570
document changes to Sledgehammer and "try"
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43569
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43568
clarify warning message to avoid confusing beginners