| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 11:20:09 +0200 |
blanchet |
delect installed ATPs dynamically, _not_ at image built time
|
file |
diff |
annotate
|
| Sat, 01 May 2010 21:29:03 +0200 |
krauss |
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:00:30 +0200 |
blanchet |
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 17:44:33 +0200 |
blanchet |
make Sledgehammer more friendly if no subgoal is left
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:17:04 +0200 |
blanchet |
rename options
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:04:20 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 14:40:36 +0200 |
blanchet |
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:12:49 +0200 |
blanchet |
remove some bloat
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:06:41 +0200 |
blanchet |
renamed module "ATP_Wrapper" to "ATP_Systems"
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 17:38:25 +0200 |
blanchet |
move the minimizer to the Sledgehammer directory
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 16:55:51 +0200 |
blanchet |
move some sledgehammer stuff out of "atp_manager.ML"
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 16:15:35 +0200 |
blanchet |
move the Sledgehammer menu options to "sledgehammer_isar.ML"
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 16:30:54 +0200 |
blanchet |
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 16:21:19 +0200 |
blanchet |
pass relevant options from "sledgehammer" to "sledgehammer minimize";
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 16:04:36 +0200 |
blanchet |
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)
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:18:05 +0200 |
blanchet |
by default, don't try to start ATPs that aren't installed
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 20:51:15 +0200 |
blanchet |
fiddle with Sledgehammer option syntax
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 16:13:49 +0200 |
blanchet |
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 21:22:13 +0200 |
blanchet |
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 |
blanchet |
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 |
blanchet |
make Sledgehammer's "timeout" option work for "minimize"
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 16:50:25 +0200 |
blanchet |
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 19:49:57 +0200 |
blanchet |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 18:44:24 +0200 |
blanchet |
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:21:51 +0200 |
blanchet |
made "theory_const" a Sledgehammer option;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:01:00 +0200 |
blanchet |
added "respect_no_atp" and "convergence" options to Sledgehammer;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 18:39:27 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 17:55:55 +0100 |
blanchet |
make Mirabelle happy again
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 14:51:36 +0100 |
blanchet |
revert debugging output that shouldn't have been submitted in the first place
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:30:33 +0100 |
blanchet |
honor the newly introduced Sledgehammer parameters and fixed the parsing;
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 14:43:22 +0100 |
blanchet |
added a syntax for specifying facts to Sledgehammer;
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 15:23:18 +0100 |
blanchet |
make "sledgehammer" and "atp_minimize" improper commands
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
file |
diff |
annotate
|