| Sat, 22 Jan 2022 14:00:36 +0100 |
desharna |
optimized app_op_level selection in TPTP generation
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:08:51 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 15:30:03 +0200 |
desharna |
proper constants in TPTP $let binding
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Fri, 18 Jan 2013 14:33:16 +0100 |
blanchet |
pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
use metaquantification when possible in Isar proofs
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 13:03:29 +0200 |
wenzelm |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 15:54:18 +0200 |
blanchet |
fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
optimized MaSh output by chunking it
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
drastic overhaul of MaSh data structures + fixed a few performance issues
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
gracefully compute cardinality of sets (to avoid type protectors)
|
file |
diff |
annotate
|
| Thu, 24 May 2012 18:21:54 +0200 |
blanchet |
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
make higher-order goals more first-order via extensionality
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
added "ext_cong_neq" lemma (not used yet); tuning
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tuning (in particular, Symtab instead of AList)
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 16:56:25 +0100 |
wenzelm |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 17:09:08 +0100 |
blanchet |
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 10:38:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|