| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| 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
|