| Sun, 03 May 2015 22:15:29 +0200 |
blanchet |
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 18:36:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 10:35:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 22:30:57 +0100 |
wenzelm |
more position information;
|
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
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
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
|
| Mon, 08 Sep 2014 14:04:03 +0200 |
blanchet |
never include hidden names -- these cannot be referenced afterward
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 20:05:39 +0200 |
blanchet |
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 21:11:08 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
whitespace tuning
|
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
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
| Wed, 28 May 2014 17:42:36 +0200 |
blanchet |
more generous max number of suggestions, for more safety
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 12:23:59 +0100 |
wenzelm |
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 18:06:23 +0100 |
wenzelm |
clarified Args.check_src: retain name space information for error output;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:20:41 +0100 |
wenzelm |
prefer Name_Space.pretty with its builtin markup;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 26 Jan 2014 13:45:40 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 22:06:07 +0100 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| Thu, 02 Jan 2014 19:07:36 +0100 |
blanchet |
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 00:05:31 +0200 |
blanchet |
make sure add: doesn't add duplicates, and works for [no_atp] facts
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 23:41:00 +0200 |
blanchet |
no fact subsumption -- this only confuses later code, e.g. 'add:'
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 15:26:58 +0200 |
blanchet |
drop only real duplicates, not subsumed facts -- this confuses MaSh
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 16:38:48 +0200 |
blanchet |
normalize more equalities
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 08:28:36 +0200 |
blanchet |
added TODO
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 08:12:53 +0200 |
blanchet |
crank up limit a bit -- truly huge background theories are still nearly 3 times larger
|
file |
diff |
annotate
|
| Tue, 08 Oct 2013 21:19:46 +0200 |
blanchet |
minor fact filter speedups
|
file |
diff |
annotate
|
| Tue, 08 Oct 2013 20:56:35 +0200 |
blanchet |
more gracefully handle huge theories in relevance filters
|
file |
diff |
annotate
|
| Tue, 08 Oct 2013 16:40:03 +0200 |
blanchet |
further optimization in relevance filter
|
file |
diff |
annotate
|
| Tue, 08 Oct 2013 14:53:33 +0200 |
blanchet |
further speed up duplicate elimination
|
file |
diff |
annotate
|
| Tue, 08 Oct 2013 14:41:25 +0200 |
blanchet |
more efficient theorem variable normalization
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 22:54:42 +0200 |
blanchet |
strengthen top sort check
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 11:02:42 +0200 |
blanchet |
encode goal digest in spying log (to detect duplicates)
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 18:37:47 +0200 |
blanchet |
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:07:24 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:07:24 +0200 |
blanchet |
disable some checks for huge background theories
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:07:24 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:07:24 +0200 |
blanchet |
reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:07:24 +0200 |
blanchet |
reverted f99ee3adb81d -- that old logic seems to make a difference still today
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:52 +0200 |
blanchet |
faster detection of tautologies
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
slight speed optimization
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of another slowdown factor in relevance filter
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
removed completely needless, inefficient code
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
minor speed optimization
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
avoid double traversal of term
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
got rid of old, needless logic
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
faster uniquification
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
stronger fact normalization
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
gracefully handle huge thys
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 15:56:51 +0200 |
blanchet |
speed up detection of simp rules
|
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
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:20 +0100 |
blanchet |
make name table work the way it was intended to
|
file |
diff |
annotate
|
| Sun, 06 Jan 2013 17:38:29 +0100 |
blanchet |
put single-theorem names before multi-theorem ones (broken since 5d147d492792)
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 11:24:09 +0100 |
blanchet |
tuned blacklisting in relevance filter
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:20 +0100 |
blanchet |
refined class handling, to prevent cycles in fact graph
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:19 +0100 |
blanchet |
learn from low-level, inside-class facts
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:19 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
add a timeout in induction rule instantiation
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 23:47:01 +0100 |
blanchet |
get rid of some junk facts in the MaSh evaluation driver
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:48:29 +0100 |
blanchet |
tweaked which facts are included for MaSh evaluations
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:48:29 +0100 |
blanchet |
don't query blacklisted theorems in evaluation driver
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:48:29 +0100 |
blanchet |
export a pair of ML functions
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 15:38:47 +0100 |
blanchet |
further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 15:25:17 +0100 |
blanchet |
better tautology check -- don't reject "prod_cases3" for example
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 13:28:23 +0100 |
blanchet |
really all facts means really all facts (well, almost)
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 02:47:45 +0100 |
blanchet |
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 00:14:58 +0100 |
blanchet |
push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 21:54:28 +0100 |
blanchet |
don't blacklist "case" theorems -- this causes problems in MaSh later
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 14:46:42 +0100 |
blanchet |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 12:06:56 +0100 |
blanchet |
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 11:52:37 +0100 |
blanchet |
centralized term printing code
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 11:32:22 +0100 |
blanchet |
thread context correctly when printing backquoted facts
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
rule out same "technical" theories for MePo as for MaSh
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
repaired accessibility chains generated by MaSh exporter + tuned one function out
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
minimal maxes + tuning
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
optimize parent computation in MaSh + remove temporary files
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
don't include hidden facts in relevance filter + tweak MaSh learning
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more work on MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
gracefully handle the case of empty theories when going up the accessibility chain
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
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 |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|