| 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
|