| Fri, 06 Mar 2015 23:44:57 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 24 Jan 2015 22:00:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 13:36:19 +0100 |
wenzelm |
prefer explicit Keyword.keywords;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:48:46 +0200 |
blanchet |
reworked unskolemization for SPASS
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 19:07:10 +0200 |
blanchet |
prefer '0.2 ms' to '249 \<mu>s'
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 17:25:56 +0200 |
blanchet |
fixed second computations
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
show microseconds as well (useful when playing with Isar proofs)
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
|
file |
diff |
annotate
|
| Sat, 12 Jul 2014 11:31:23 +0200 |
blanchet |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
file |
diff |
annotate
|
| Thu, 10 Jul 2014 18:08:21 +0200 |
blanchet |
lambda-lifting for Z3 Isar proofs
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:05:44 +0100 |
blanchet |
more simplification of trivial steps
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:18:52 +0100 |
blanchet |
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 20:09:13 +0100 |
blanchet |
simplify generated propositions
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 19:01:06 +0100 |
blanchet |
use 'prop' rather than 'bool' systematically in Isar reconstruction code
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
eliminated Sledgehammer's dependency on old-style datatypes
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 16:02:02 +0200 |
blanchet |
sorted out dependencies
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
moved ML function closer to its remaining use
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
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
|
| Mon, 20 May 2013 13:07:31 +0200 |
blanchet |
parse agsyHOL proofs (as unsat cores)
|
file |
diff |
annotate
|
| Mon, 20 May 2013 12:35:29 +0200 |
blanchet |
freeze types in Sledgehammer goal, not just terms
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 17:12:21 +0100 |
blanchet |
more simplifying constructors
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 10:45:23 +0100 |
blanchet |
optimize Isar output some more
|
file |
diff |
annotate
|