Fri, 16 Apr 2010 16:13:49 +0200 |
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
|
file | diff | annotate |
Wed, 14 Apr 2010 21:22:13 +0200 |
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
|
file | diff | annotate |
Wed, 14 Apr 2010 18:23:51 +0200 |
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
|
file | diff | annotate |
Wed, 14 Apr 2010 17:10:16 +0200 |
make Sledgehammer's "timeout" option work for "minimize"
|
file | diff | annotate |
Wed, 14 Apr 2010 16:50:25 +0200 |
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
|
file | diff | annotate |
Mon, 29 Mar 2010 19:49:57 +0200 |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file | diff | annotate |
Mon, 29 Mar 2010 18:44:24 +0200 |
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
|
file | diff | annotate |
Mon, 29 Mar 2010 12:21:51 +0200 |
made "theory_const" a Sledgehammer option;
|
file | diff | annotate |
Mon, 29 Mar 2010 12:01:00 +0200 |
added "respect_no_atp" and "convergence" options to Sledgehammer;
|
file | diff | annotate |
Sun, 28 Mar 2010 18:39:27 +0200 |
make SML/NJ happy
|
file | diff | annotate |
Thu, 25 Mar 2010 17:55:55 +0100 |
make Mirabelle happy again
|
file | diff | annotate |
Wed, 24 Mar 2010 14:51:36 +0100 |
revert debugging output that shouldn't have been submitted in the first place
|
file | diff | annotate |
Wed, 24 Mar 2010 12:30:33 +0100 |
honor the newly introduced Sledgehammer parameters and fixed the parsing;
|
file | diff | annotate |
Tue, 23 Mar 2010 14:43:22 +0100 |
added a syntax for specifying facts to Sledgehammer;
|
file | diff | annotate |
Tue, 23 Mar 2010 11:39:21 +0100 |
added options to Sledgehammer;
|
file | diff | annotate |
Mon, 22 Mar 2010 15:23:18 +0100 |
make "sledgehammer" and "atp_minimize" improper commands
|
file | diff | annotate |
Fri, 19 Mar 2010 15:07:44 +0100 |
move the Sledgehammer Isar commands together into one file;
|
file | diff | annotate |