Tue, 20 Apr 2010 14:39:42 +0200 |
blanchet |
merge
|
changeset |
files
|
Mon, 19 Apr 2010 19:41:30 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
Mon, 19 Apr 2010 19:41:15 +0200 |
blanchet |
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
|
changeset |
files
|
Mon, 19 Apr 2010 18:44:12 +0200 |
blanchet |
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
|
changeset |
files
|
Mon, 19 Apr 2010 18:14:45 +0200 |
blanchet |
added warning about inconsistent context to Metis;
|
changeset |
files
|
Mon, 19 Apr 2010 17:18:21 +0200 |
blanchet |
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
|
changeset |
files
|
Mon, 19 Apr 2010 16:33:48 +0200 |
blanchet |
got rid of somewhat pointless "pairname" function in Sledgehammer
|
changeset |
files
|
Mon, 19 Apr 2010 16:33:20 +0200 |
blanchet |
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
|
changeset |
files
|
Mon, 19 Apr 2010 16:29:52 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
Mon, 19 Apr 2010 15:24:57 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
Mon, 19 Apr 2010 15:21:35 +0200 |
blanchet |
cosmetics
|
changeset |
files
|
Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
changeset |
files
|
Mon, 19 Apr 2010 11:54:07 +0200 |
blanchet |
don't use readable names if proof reconstruction is needed, because it uses the structure of names
|
changeset |
files
|
Mon, 19 Apr 2010 11:02:00 +0200 |
blanchet |
allow "_" in TPTP names in debug mode
|
changeset |
files
|
Mon, 19 Apr 2010 10:45:08 +0200 |
blanchet |
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
|
changeset |
files
|
Mon, 19 Apr 2010 10:15:02 +0200 |
blanchet |
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
|
changeset |
files
|
Mon, 19 Apr 2010 09:53:31 +0200 |
blanchet |
get rid of "List.foldl" + add timestamp to SPASS
|
changeset |
files
|
Tue, 20 Apr 2010 15:17:18 +0200 |
wenzelm |
less ambitious settings for cygwin-poly;
|
changeset |
files
|
Tue, 20 Apr 2010 14:56:58 +0200 |
Cezary Kaliszyk |
respectfullness and preservation of map for identity quotients
|
changeset |
files
|
Tue, 20 Apr 2010 14:56:20 +0200 |
Cezary Kaliszyk |
respectfullness and preservation of function composition
|
changeset |
files
|
Tue, 20 Apr 2010 14:55:53 +0200 |
Cezary Kaliszyk |
eta-normalize the goal since the original theorem is atomized
|
changeset |
files
|
Tue, 20 Apr 2010 11:31:14 +0200 |
wenzelm |
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
|
changeset |
files
|
Tue, 20 Apr 2010 11:26:25 +0200 |
wenzelm |
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
|
changeset |
files
|
Tue, 20 Apr 2010 06:53:50 +0200 |
haftmann |
merged
|
changeset |
files
|
Mon, 19 Apr 2010 15:31:58 +0200 |
haftmann |
more appropriate representation of valid positions for abstractors
|
changeset |
files
|
Mon, 19 Apr 2010 15:31:56 +0200 |
haftmann |
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
|
changeset |
files
|
Mon, 19 Apr 2010 23:11:39 +0200 |
wenzelm |
update_syntax: add new productions only once, to allow repeated local notation, for example;
|
changeset |
files
|
Mon, 19 Apr 2010 17:57:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 19 Apr 2010 17:31:48 +0200 |
wenzelm |
more platform information;
|
changeset |
files
|
Mon, 19 Apr 2010 17:27:41 +0200 |
wenzelm |
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
|
changeset |
files
|
Mon, 19 Apr 2010 16:04:42 +0200 |
wenzelm |
some updates on multi-platform support;
|
changeset |
files
|
Mon, 19 Apr 2010 12:15:06 +0200 |
haftmann |
merged
|
changeset |
files
|
Mon, 19 Apr 2010 11:30:08 +0200 |
haftmann |
explicit check sorts in abstract certificates; abstractor is part of dependencies
|
changeset |
files
|
Mon, 19 Apr 2010 10:56:26 +0200 |
wenzelm |
polyml-platform script is superseded by ISABELLE_PLATFORM;
|
changeset |
files
|
Mon, 19 Apr 2010 10:19:37 +0200 |
wenzelm |
less ambitious settings for cygwin-poly;
|
changeset |
files
|
Mon, 19 Apr 2010 07:38:35 +0200 |
haftmann |
merged
|
changeset |
files
|
Mon, 19 Apr 2010 07:38:08 +0200 |
haftmann |
more convenient equations for zip
|
changeset |
files
|
Sat, 17 Apr 2010 23:05:52 +0200 |
wenzelm |
more platform info;
|
changeset |
files
|
Sat, 17 Apr 2010 22:58:29 +0200 |
wenzelm |
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
|
changeset |
files
|
Sat, 17 Apr 2010 21:40:29 +0200 |
wenzelm |
system properties determine the JVM platform, not the Isabelle one;
|
changeset |
files
|
Sat, 17 Apr 2010 21:01:55 +0200 |
wenzelm |
THIS_CYGWIN;
|
changeset |
files
|
Sat, 17 Apr 2010 20:42:26 +0200 |
wenzelm |
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
|
changeset |
files
|
Sat, 17 Apr 2010 19:35:35 +0200 |
wenzelm |
isatest: more robust treatment of remote files, less reliance on mounted file system;
|
changeset |
files
|
Sat, 17 Apr 2010 11:05:22 +0200 |
blanchet |
merged
|
changeset |
files
|
Sat, 17 Apr 2010 10:42:09 +0200 |
blanchet |
added missing \n in output
|
changeset |
files
|
Fri, 16 Apr 2010 21:18:05 +0200 |
blanchet |
by default, don't try to start ATPs that aren't installed
|
changeset |
files
|
Fri, 16 Apr 2010 20:51:15 +0200 |
blanchet |
fiddle with Sledgehammer option syntax
|
changeset |
files
|
Fri, 16 Apr 2010 20:50:50 +0200 |
blanchet |
added timestamp to proof
|
changeset |
files
|
Fri, 16 Apr 2010 16:54:05 +0200 |
blanchet |
restore order of clauses in TPTP output;
|
changeset |
files
|
Fri, 16 Apr 2010 16:53:00 +0200 |
blanchet |
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
|
changeset |
files
|
Fri, 16 Apr 2010 16:51:54 +0200 |
blanchet |
output total time taken by Sledgehammer if "verbose" is set
|
changeset |
files
|
Fri, 16 Apr 2010 16:13:49 +0200 |
blanchet |
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
|
changeset |
files
|
Fri, 16 Apr 2010 16:08:43 +0200 |
blanchet |
reorganize Sledgehammer's relevance filter slightly
|
changeset |
files
|
Fri, 16 Apr 2010 15:59:53 +0200 |
blanchet |
tell the user that Sledgehammer kills its siblings
|
changeset |
files
|
Fri, 16 Apr 2010 22:52:49 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
Fri, 16 Apr 2010 22:45:07 +0200 |
wenzelm |
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
|
changeset |
files
|
Fri, 16 Apr 2010 22:18:59 +0200 |
wenzelm |
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
|
changeset |
files
|
Fri, 16 Apr 2010 22:15:09 +0200 |
wenzelm |
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
|
changeset |
files
|
Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
changeset |
files
|
Fri, 16 Apr 2010 20:56:40 +0200 |
wenzelm |
allow syntax types within abbreviations;
|
changeset |
files
|