blanchet [Wed, 21 Apr 2010 16:38:03 +0200] rev 36282
generate command-line in addition to timestamp in ATP output file, for debugging purposes
blanchet [Wed, 21 Apr 2010 16:21:19 +0200] rev 36281
pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Apr 2010 10:00:53 +0200] rev 36280
Finite set theory
wenzelm [Thu, 22 Apr 2010 22:12:12 +0200] rev 36279
merged
paulson [Thu, 22 Apr 2010 20:39:48 +0100] rev 36278
Tidied up using s/l
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
blanchet [Mon, 19 Apr 2010 11:02:00 +0200] rev 36221
allow "_" in TPTP names in debug mode
blanchet [Mon, 19 Apr 2010 10:45:08 +0200] rev 36220
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet [Mon, 19 Apr 2010 10:15:02 +0200] rev 36219
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet [Mon, 19 Apr 2010 09:53:31 +0200] rev 36218
get rid of "List.foldl" + add timestamp to SPASS
wenzelm [Tue, 20 Apr 2010 15:17:18 +0200] rev 36217
less ambitious settings for cygwin-poly;
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:58 +0200] rev 36216
respectfullness and preservation of map for identity quotients
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:20 +0200] rev 36215
respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:55:53 +0200] rev 36214
eta-normalize the goal since the original theorem is atomized
wenzelm [Tue, 20 Apr 2010 11:31:14 +0200] rev 36213
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
wenzelm [Tue, 20 Apr 2010 11:26:25 +0200] rev 36212
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
haftmann [Tue, 20 Apr 2010 06:53:50 +0200] rev 36211
merged
haftmann [Mon, 19 Apr 2010 15:31:58 +0200] rev 36210
more appropriate representation of valid positions for abstractors
haftmann [Mon, 19 Apr 2010 15:31:56 +0200] rev 36209
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
wenzelm [Mon, 19 Apr 2010 23:11:39 +0200] rev 36208
update_syntax: add new productions only once, to allow repeated local notation, for example;
wenzelm [Mon, 19 Apr 2010 17:57:07 +0200] rev 36207
tuned;
wenzelm [Mon, 19 Apr 2010 17:31:48 +0200] rev 36206
more platform information;
wenzelm [Mon, 19 Apr 2010 17:27:41 +0200] rev 36205
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
wenzelm [Mon, 19 Apr 2010 16:04:42 +0200] rev 36204
some updates on multi-platform support;
haftmann [Mon, 19 Apr 2010 12:15:06 +0200] rev 36203
merged
haftmann [Mon, 19 Apr 2010 11:30:08 +0200] rev 36202
explicit check sorts in abstract certificates; abstractor is part of dependencies
wenzelm [Mon, 19 Apr 2010 10:56:26 +0200] rev 36201
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm [Mon, 19 Apr 2010 10:19:37 +0200] rev 36200
less ambitious settings for cygwin-poly;
haftmann [Mon, 19 Apr 2010 07:38:35 +0200] rev 36199
merged
haftmann [Mon, 19 Apr 2010 07:38:08 +0200] rev 36198
more convenient equations for zip
wenzelm [Sat, 17 Apr 2010 23:05:52 +0200] rev 36197
more platform info;
wenzelm [Sat, 17 Apr 2010 22:58:29 +0200] rev 36196
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm [Sat, 17 Apr 2010 21:40:29 +0200] rev 36195
system properties determine the JVM platform, not the Isabelle one;
wenzelm [Sat, 17 Apr 2010 21:01:55 +0200] rev 36194
THIS_CYGWIN;
wenzelm [Sat, 17 Apr 2010 20:42:26 +0200] rev 36193
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm [Sat, 17 Apr 2010 19:35:35 +0200] rev 36192
isatest: more robust treatment of remote files, less reliance on mounted file system;
blanchet [Sat, 17 Apr 2010 11:05:22 +0200] rev 36191
merged
blanchet [Sat, 17 Apr 2010 10:42:09 +0200] rev 36190
added missing \n in output
blanchet [Fri, 16 Apr 2010 21:18:05 +0200] rev 36189
by default, don't try to start ATPs that aren't installed
blanchet [Fri, 16 Apr 2010 20:51:15 +0200] rev 36188
fiddle with Sledgehammer option syntax
blanchet [Fri, 16 Apr 2010 20:50:50 +0200] rev 36187
added timestamp to proof