Wed, 21 Apr 2010 16:38:03 +0200 generate command-line in addition to timestamp in ATP output file, for debugging purposes
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
Wed, 21 Apr 2010 16:21:19 +0200 pass relevant options from "sledgehammer" to "sledgehammer minimize";
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
Fri, 23 Apr 2010 10:00:53 +0200 Finite set theory
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Apr 2010 10:00:53 +0200] rev 36280
Finite set theory
Thu, 22 Apr 2010 22:12:12 +0200 merged
wenzelm [Thu, 22 Apr 2010 22:12:12 +0200] rev 36279
merged
Thu, 22 Apr 2010 20:39:48 +0100 Tidied up using s/l
paulson [Thu, 22 Apr 2010 20:39:48 +0100] rev 36278
Tidied up using s/l
Thu, 22 Apr 2010 22:01:06 +0200 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;
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;
Thu, 22 Apr 2010 11:55:19 +0200 fun_rel introduction and list_rel elimination for quotient package
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
Thu, 22 Apr 2010 09:30:39 +0200 lemmas concerning remdups
haftmann [Thu, 22 Apr 2010 09:30:39 +0200] rev 36275
lemmas concerning remdups
Thu, 22 Apr 2010 09:30:36 +0200 lemma dlist_ext
haftmann [Thu, 22 Apr 2010 09:30:36 +0200] rev 36274
lemma dlist_ext
Wed, 21 Apr 2010 21:11:26 +0200 merged
haftmann [Wed, 21 Apr 2010 21:11:26 +0200] rev 36273
merged
Wed, 21 Apr 2010 15:20:59 +0200 optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann [Wed, 21 Apr 2010 15:20:59 +0200] rev 36272
optionally ignore errors during translation of equations; tuned representation of abstraction points
Wed, 21 Apr 2010 15:20:57 +0200 optionally ignore errors during translation of equations
haftmann [Wed, 21 Apr 2010 15:20:57 +0200] rev 36271
optionally ignore errors during translation of equations
Wed, 21 Apr 2010 15:45:33 +0200 tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss [Wed, 21 Apr 2010 15:45:33 +0200] rev 36270
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
Wed, 21 Apr 2010 15:37:39 +0200 simplified example
krauss [Wed, 21 Apr 2010 15:37:39 +0200] rev 36269
simplified example
Wed, 21 Apr 2010 14:46:29 +0200 use only one thread in "Manual_Nits";
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
Wed, 21 Apr 2010 14:02:34 +0200 merged
blanchet [Wed, 21 Apr 2010 14:02:34 +0200] rev 36267
merged
Wed, 21 Apr 2010 14:02:19 +0200 clarify error message
blanchet [Wed, 21 Apr 2010 14:02:19 +0200] rev 36266
clarify error message
Wed, 21 Apr 2010 12:22:04 +0200 distinguish between the different ATP errors in the user interface;
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
Wed, 21 Apr 2010 11:03:35 +0200 added "spass_tptp" prover, which requires SPASS x.y > 3.0;
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"
Tue, 20 Apr 2010 17:41:00 +0200 use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
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"
Wed, 21 Apr 2010 12:11:48 +0200 merged
bulwahn [Wed, 21 Apr 2010 12:11:48 +0200] rev 36262
merged
Wed, 21 Apr 2010 12:10:53 +0200 make profiling depend on reference Quickcheck.timing
bulwahn [Wed, 21 Apr 2010 12:10:53 +0200] rev 36261
make profiling depend on reference Quickcheck.timing
Wed, 21 Apr 2010 12:10:52 +0200 added examples for detecting switches
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36260
added examples for detecting switches
Wed, 21 Apr 2010 12:10:52 +0200 adopting documentation of the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36259
adopting documentation of the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 removing dead code; clarifying function names; removing clone
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36258
removing dead code; clarifying function names; removing clone
Wed, 21 Apr 2010 12:10:52 +0200 adopting examples to changes in the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36257
adopting examples to changes in the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 adopting quickcheck
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36256
adopting quickcheck
Wed, 21 Apr 2010 12:10:52 +0200 tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36255
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
Wed, 21 Apr 2010 12:10:52 +0200 added switch detection to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36254
added switch detection to the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 added further inlining of boolean constants 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
Wed, 21 Apr 2010 12:10:52 +0200 adding more profiling to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36252
adding more profiling to the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 only add relevant predicates to the list of extra modes
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36251
only add relevant predicates to the list of extra modes
Wed, 21 Apr 2010 12:10:52 +0200 switched off no_topmost_reordering
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36250
switched off no_topmost_reordering
Wed, 21 Apr 2010 12:10:52 +0200 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 36249
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 added option for specialisation to the predicate compiler
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36248
added option for specialisation to the predicate compiler
Wed, 21 Apr 2010 12:10:52 +0200 prefer functional modes of functions in the mode analysis
bulwahn [Wed, 21 Apr 2010 12:10:52 +0200] rev 36247
prefer functional modes of functions in the mode analysis
Wed, 21 Apr 2010 12:10:52 +0200 added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
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
Wed, 21 Apr 2010 11:23:04 +0200 merged
hoelzl [Wed, 21 Apr 2010 11:23:04 +0200] rev 36245
merged
Wed, 21 Apr 2010 10:44:44 +0200 Only use provided SMT-certificates in HOL-Multivariate_Analysis.
hoelzl [Wed, 21 Apr 2010 10:44:44 +0200] rev 36244
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
Tue, 20 Apr 2010 14:07:52 +0200 Translated remaining theorems about integration from HOL light.
himmelma [Tue, 20 Apr 2010 14:07:52 +0200] rev 36243
Translated remaining theorems about integration from HOL light.
Wed, 21 Apr 2010 11:11:42 +0200 marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
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.);
Tue, 20 Apr 2010 13:44:28 -0700 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman [Tue, 20 Apr 2010 13:44:28 -0700] rev 36241
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
Tue, 20 Apr 2010 22:34:17 +0200 Remove garbage.
ballarin [Tue, 20 Apr 2010 22:34:17 +0200] rev 36240
Remove garbage.
Tue, 20 Apr 2010 22:31:08 +0200 Remove garbage.
ballarin [Tue, 20 Apr 2010 22:31:08 +0200] rev 36239
Remove garbage.
Tue, 20 Apr 2010 17:07:53 +0200 recovered isabelle java, which was broken in ebfa4bb0d50f;
wenzelm [Tue, 20 Apr 2010 17:07:53 +0200] rev 36238
recovered isabelle java, which was broken in ebfa4bb0d50f;
Tue, 20 Apr 2010 16:14:45 +0200 fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
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
Tue, 20 Apr 2010 16:04:49 +0200 merged
blanchet [Tue, 20 Apr 2010 16:04:49 +0200] rev 36236
merged
Tue, 20 Apr 2010 16:04:36 +0200 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 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)
Tue, 20 Apr 2010 14:39:42 +0200 merge
blanchet [Tue, 20 Apr 2010 14:39:42 +0200] rev 36234
merge
Mon, 19 Apr 2010 19:41:30 +0200 cosmetics
blanchet [Mon, 19 Apr 2010 19:41:30 +0200] rev 36233
cosmetics
Mon, 19 Apr 2010 19:41:15 +0200 don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
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
Mon, 19 Apr 2010 18:44:12 +0200 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: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
Mon, 19 Apr 2010 18:14:45 +0200 added warning about inconsistent context to Metis;
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
Mon, 19 Apr 2010 17:18:21 +0200 workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
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
Mon, 19 Apr 2010 16:33:48 +0200 got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet [Mon, 19 Apr 2010 16:33:48 +0200] rev 36228
got rid of somewhat pointless "pairname" function in Sledgehammer
Mon, 19 Apr 2010 16:33:20 +0200 make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
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
Mon, 19 Apr 2010 16:29:52 +0200 cosmetics
blanchet [Mon, 19 Apr 2010 16:29:52 +0200] rev 36226
cosmetics
Mon, 19 Apr 2010 15:24:57 +0200 cosmetics
blanchet [Mon, 19 Apr 2010 15:24:57 +0200] rev 36225
cosmetics
Mon, 19 Apr 2010 15:21:35 +0200 cosmetics
blanchet [Mon, 19 Apr 2010 15:21:35 +0200] rev 36224
cosmetics
Mon, 19 Apr 2010 15:15:21 +0200 make Sledgehammer's minimizer also minimize Isar proofs
blanchet [Mon, 19 Apr 2010 15:15:21 +0200] rev 36223
make Sledgehammer's minimizer also minimize Isar proofs
Mon, 19 Apr 2010 11:54:07 +0200 don't use readable names if proof reconstruction is needed, because it uses the structure of names
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
Mon, 19 Apr 2010 11:02:00 +0200 allow "_" in TPTP names in debug mode
blanchet [Mon, 19 Apr 2010 11:02:00 +0200] rev 36221
allow "_" in TPTP names in debug mode
Mon, 19 Apr 2010 10:45:08 +0200 rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
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
Mon, 19 Apr 2010 10:15:02 +0200 set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
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
Mon, 19 Apr 2010 09:53:31 +0200 get rid of "List.foldl" + add timestamp to SPASS
blanchet [Mon, 19 Apr 2010 09:53:31 +0200] rev 36218
get rid of "List.foldl" + add timestamp to SPASS
Tue, 20 Apr 2010 15:17:18 +0200 less ambitious settings for cygwin-poly;
wenzelm [Tue, 20 Apr 2010 15:17:18 +0200] rev 36217
less ambitious settings for cygwin-poly;
Tue, 20 Apr 2010 14:56:58 +0200 respectfullness and preservation of map for identity quotients
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:58 +0200] rev 36216
respectfullness and preservation of map for identity quotients
Tue, 20 Apr 2010 14:56:20 +0200 respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 20 Apr 2010 14:56:20 +0200] rev 36215
respectfullness and preservation of function composition
Tue, 20 Apr 2010 14:55:53 +0200 eta-normalize the goal since the original theorem is atomized
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
Tue, 20 Apr 2010 11:31:14 +0200 accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
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;
Tue, 20 Apr 2010 11:26:25 +0200 refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
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;
Tue, 20 Apr 2010 06:53:50 +0200 merged
haftmann [Tue, 20 Apr 2010 06:53:50 +0200] rev 36211
merged
Mon, 19 Apr 2010 15:31:58 +0200 more appropriate representation of valid positions for abstractors
haftmann [Mon, 19 Apr 2010 15:31:58 +0200] rev 36210
more appropriate representation of valid positions for abstractors
Mon, 19 Apr 2010 15:31:56 +0200 more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
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
Mon, 19 Apr 2010 23:11:39 +0200 update_syntax: add new productions only once, to allow repeated local notation, for example;
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;
Mon, 19 Apr 2010 17:57:07 +0200 tuned;
wenzelm [Mon, 19 Apr 2010 17:57:07 +0200] rev 36207
tuned;
Mon, 19 Apr 2010 17:31:48 +0200 more platform information;
wenzelm [Mon, 19 Apr 2010 17:31:48 +0200] rev 36206
more platform information;
Mon, 19 Apr 2010 17:27:41 +0200 check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
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;
Mon, 19 Apr 2010 16:04:42 +0200 some updates on multi-platform support;
wenzelm [Mon, 19 Apr 2010 16:04:42 +0200] rev 36204
some updates on multi-platform support;
Mon, 19 Apr 2010 12:15:06 +0200 merged
haftmann [Mon, 19 Apr 2010 12:15:06 +0200] rev 36203
merged
Mon, 19 Apr 2010 11:30:08 +0200 explicit check sorts in abstract certificates; abstractor is part of dependencies
haftmann [Mon, 19 Apr 2010 11:30:08 +0200] rev 36202
explicit check sorts in abstract certificates; abstractor is part of dependencies
Mon, 19 Apr 2010 10:56:26 +0200 polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm [Mon, 19 Apr 2010 10:56:26 +0200] rev 36201
polyml-platform script is superseded by ISABELLE_PLATFORM;
Mon, 19 Apr 2010 10:19:37 +0200 less ambitious settings for cygwin-poly;
wenzelm [Mon, 19 Apr 2010 10:19:37 +0200] rev 36200
less ambitious settings for cygwin-poly;
Mon, 19 Apr 2010 07:38:35 +0200 merged
haftmann [Mon, 19 Apr 2010 07:38:35 +0200] rev 36199
merged
Mon, 19 Apr 2010 07:38:08 +0200 more convenient equations for zip
haftmann [Mon, 19 Apr 2010 07:38:08 +0200] rev 36198
more convenient equations for zip
Sat, 17 Apr 2010 23:05:52 +0200 more platform info;
wenzelm [Sat, 17 Apr 2010 23:05:52 +0200] rev 36197
more platform info;
Sat, 17 Apr 2010 22:58:29 +0200 added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
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;
Sat, 17 Apr 2010 21:40:29 +0200 system properties determine the JVM platform, not the Isabelle one;
wenzelm [Sat, 17 Apr 2010 21:40:29 +0200] rev 36195
system properties determine the JVM platform, not the Isabelle one;
Sat, 17 Apr 2010 21:01:55 +0200 THIS_CYGWIN;
wenzelm [Sat, 17 Apr 2010 21:01:55 +0200] rev 36194
THIS_CYGWIN;
Sat, 17 Apr 2010 20:42:26 +0200 improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm [Sat, 17 Apr 2010 20:42:26 +0200] rev 36193
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
Sat, 17 Apr 2010 19:35:35 +0200 isatest: more robust treatment of remote files, less reliance on mounted file system;
wenzelm [Sat, 17 Apr 2010 19:35:35 +0200] rev 36192
isatest: more robust treatment of remote files, less reliance on mounted file system;
Sat, 17 Apr 2010 11:05:22 +0200 merged
blanchet [Sat, 17 Apr 2010 11:05:22 +0200] rev 36191
merged
Sat, 17 Apr 2010 10:42:09 +0200 added missing \n in output
blanchet [Sat, 17 Apr 2010 10:42:09 +0200] rev 36190
added missing \n in output
Fri, 16 Apr 2010 21:18:05 +0200 by default, don't try to start ATPs that aren't installed
blanchet [Fri, 16 Apr 2010 21:18:05 +0200] rev 36189
by default, don't try to start ATPs that aren't installed
Fri, 16 Apr 2010 20:51:15 +0200 fiddle with Sledgehammer option syntax
blanchet [Fri, 16 Apr 2010 20:51:15 +0200] rev 36188
fiddle with Sledgehammer option syntax
Fri, 16 Apr 2010 20:50:50 +0200 added timestamp to proof
blanchet [Fri, 16 Apr 2010 20:50:50 +0200] rev 36187
added timestamp to proof
(0) -30000 -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip