| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2017 13:13:25 +0200 |
wenzelm |
discontinued obsolete print mode;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 22:24:37 +0100 |
blanchet |
removed needless ML function
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 22:21:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| 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
|