| Wed, 20 Oct 2021 20:25:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2020 07:28:17 +0000 |
haftmann |
hooks for foundational terms: protection of foundational terms during simplification
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 09:24:34 +0000 |
haftmann |
more direct accessors for simpset
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 21:49:06 +0100 |
wenzelm |
support for isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:31:25 +0100 |
wenzelm |
clarified signature: prefer proper order operation;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 15:46:35 +0100 |
wenzelm |
more embedded cartouche arguments;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 22:36:10 +0200 |
wenzelm |
provide Pure.simp/simp_all, which only know about meta-equality;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:23:10 +0200 |
wenzelm |
avoid warnings on duplicate rules in the given list;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Wed, 16 Dec 2015 16:31:36 +0100 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 23:01:27 +0200 |
wenzelm |
clarified declaration flags, like 'declaration' command;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 23:31:41 +0200 |
wenzelm |
eliminated pointless cterms;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
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
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
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
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 14:54:32 +0200 |
wenzelm |
more explicit Method.modifier with reported position;
|
file |
diff |
annotate
|