| Wed, 07 Aug 2019 18:23:32 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2019 17:00:07 +0200 |
wenzelm |
eliminated pointless comments;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2015 00:03:10 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 21:33:00 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +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
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 10:36:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:09:53 +0100 |
wenzelm |
more standard file/module names;
|
file |
diff |
annotate
| base
|