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