wenzelm [Thu, 22 Apr 2010 22:01:06 +0200] rev 36277
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Apr 2010 11:55:19 +0200] rev 36276
fun_rel introduction and list_rel elimination for quotient package
haftmann [Thu, 22 Apr 2010 09:30:39 +0200] rev 36275
lemmas concerning remdups
haftmann [Thu, 22 Apr 2010 09:30:36 +0200] rev 36274
lemma dlist_ext
haftmann [Wed, 21 Apr 2010 21:11:26 +0200] rev 36273
merged
haftmann [Wed, 21 Apr 2010 15:20:59 +0200] rev 36272
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann [Wed, 21 Apr 2010 15:20:57 +0200] rev 36271
optionally ignore errors during translation of equations
krauss [Wed, 21 Apr 2010 15:45:33 +0200] rev 36270
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss [Wed, 21 Apr 2010 15:37:39 +0200] rev 36269
simplified example
blanchet [Wed, 21 Apr 2010 14:46:29 +0200] rev 36268
use only one thread in "Manual_Nits";
the second thread isn't helping much, and might very well be the cause of the Cygwin Isatest failure
blanchet [Wed, 21 Apr 2010 14:02:34 +0200] rev 36267
merged
blanchet [Wed, 21 Apr 2010 14:02:19 +0200] rev 36266
clarify error message
blanchet [Wed, 21 Apr 2010 12:22:04 +0200] rev 36265
distinguish between the different ATP errors in the user interface;
in particular, tell users to upgrade their SPASS if they try to run "spass_tptp" with an old SPASS version with no TPTP support
blanchet [Wed, 21 Apr 2010 11:03:35 +0200] rev 36264
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
once users have upgraded their SPASS and we have determined that "spass_tptp" works well, we can make "spass_tptp" the one and only "spass"
blanchet [Tue, 20 Apr 2010 17:41:00 +0200] rev 36263
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
bulwahn [Wed, 21 Apr 2010 12:11:48 +0200] rev 36262
merged
bulwahn [Wed, 21 Apr 2010 12:10:53 +0200] rev 36261
make profiling depend on reference Quickcheck.timing
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36260
added examples for detecting switches
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36259
adopting documentation of the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36258
removing dead code; clarifying function names; removing clone
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36257
adopting examples to changes in the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36256
adopting quickcheck
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36255
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36254
added switch detection to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36253
added further inlining of boolean constants to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36252
adding more profiling to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36251
only add relevant predicates to the list of extra modes
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36250
switched off no_topmost_reordering
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36249
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36248
added option for specialisation to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36247
prefer functional modes of functions in the mode analysis
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36246
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
hoelzl [Wed, 21 Apr 2010 11:23:04 +0200] rev 36245
merged
hoelzl [Wed, 21 Apr 2010 10:44:44 +0200] rev 36244
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
himmelma [Tue, 20 Apr 2010 14:07:52 +0200] rev 36243
Translated remaining theorems about integration from HOL light.
wenzelm [Wed, 21 Apr 2010 11:11:42 +0200] rev 36242
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
huffman [Tue, 20 Apr 2010 13:44:28 -0700] rev 36241
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
ballarin [Tue, 20 Apr 2010 22:34:17 +0200] rev 36240
Remove garbage.
ballarin [Tue, 20 Apr 2010 22:31:08 +0200] rev 36239
Remove garbage.
wenzelm [Tue, 20 Apr 2010 17:07:53 +0200] rev 36238
recovered isabelle java, which was broken in ebfa4bb0d50f;
blanchet [Tue, 20 Apr 2010 16:14:45 +0200] rev 36237
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated
blanchet [Tue, 20 Apr 2010 16:04:49 +0200] rev 36236
merged
blanchet [Tue, 20 Apr 2010 16:04:36 +0200] rev 36235
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet [Tue, 20 Apr 2010 14:39:42 +0200] rev 36234
merge
blanchet [Mon, 19 Apr 2010 19:41:30 +0200] rev 36233
cosmetics
blanchet [Mon, 19 Apr 2010 19:41:15 +0200] rev 36232
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files
blanchet [Mon, 19 Apr 2010 18:44:12 +0200] rev 36231
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet [Mon, 19 Apr 2010 18:14:45 +0200] rev 36230
added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
blanchet [Mon, 19 Apr 2010 17:18:21 +0200] rev 36229
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
blanchet [Mon, 19 Apr 2010 16:33:48 +0200] rev 36228
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet [Mon, 19 Apr 2010 16:33:20 +0200] rev 36227
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
blanchet [Mon, 19 Apr 2010 16:29:52 +0200] rev 36226
cosmetics
blanchet [Mon, 19 Apr 2010 15:24:57 +0200] rev 36225
cosmetics
blanchet [Mon, 19 Apr 2010 15:21:35 +0200] rev 36224
cosmetics
blanchet [Mon, 19 Apr 2010 15:15:21 +0200] rev 36223
make Sledgehammer's minimizer also minimize Isar proofs
blanchet [Mon, 19 Apr 2010 11:54:07 +0200] rev 36222
don't use readable names if proof reconstruction is needed, because it uses the structure of names