| Mon, 19 Aug 2013 16:50:25 +0200 |
blanchet |
handle Bounds as well in MaSh features
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:47:47 +0200 |
blanchet |
add subtypes as well as features in MaSh
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:41:22 +0200 |
blanchet |
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:26:59 +0200 |
blanchet |
generate deep type patterns in MaSh
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Sun, 19 May 2013 20:41:19 +0200 |
blanchet |
made "completish" mode a bit more complete
|
file |
diff |
annotate
|
| Fri, 17 May 2013 11:35:52 +0200 |
wenzelm |
tuned signature -- emphasize thread creation here;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:37:07 +0100 |
blanchet |
reintroduced crucial sorting accidentally lost in 962190eab40d
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:27:33 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:21:49 +0100 |
blanchet |
provide two modes for MaSh driver: linearized or real visibility
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:55 +0100 |
blanchet |
implement (more) accurate computation of parents
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 11:33:43 +0100 |
blanchet |
tuned code: factored out parent computation
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 10:43:36 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
avoid crude/wrong theorem comparision
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
more MaSh tracing
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 08 Feb 2013 12:22:37 +0100 |
blanchet |
added option to use SNoW as machine learning algo
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
killed deadcode
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
drop needless .0s
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
file |
diff |
annotate
|
| Tue, 05 Feb 2013 17:19:13 +0100 |
blanchet |
removed spurious trimming
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|