| Sat, 21 Oct 2023 21:19:02 +0200 |
wenzelm |
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
|
file |
diff |
annotate
|
| Sat, 21 Oct 2023 12:02:23 +0200 |
wenzelm |
more robust read_simproc_spec: proper error positions;
|
file |
diff |
annotate
|
| Sat, 21 Oct 2023 11:34:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 20 Oct 2023 22:19:05 +0200 |
wenzelm |
added ML antiquotation "simproc_setup";
|
file |
diff |
annotate
|
| Fri, 20 Oct 2023 11:03:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 21:58:47 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 17:06:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 16:31:17 +0200 |
wenzelm |
clarified syntax and order of parameters;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 11:30:16 +0200 |
wenzelm |
clarified signature: Named_Target.setup works both for global and local theory;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 22:09:25 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 16:29:24 +0200 |
wenzelm |
clarified signature: more concise simproc setup in ML;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 18:55:29 +0200 |
wenzelm |
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
|
file |
diff |
annotate
|
| Sat, 27 May 2023 13:29:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 26 May 2023 13:19:49 +0200 |
wenzelm |
clarified treatment of context;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Fri, 19 May 2023 11:42:12 +0200 |
wenzelm |
remove pointless context setup (see also b2e449c155a4);
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 19:43:42 +0200 |
wenzelm |
more standard treatment of morphism context, but hardly relevant here;
|
file |
diff |
annotate
|
| Sun, 14 May 2023 13:15:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 13 May 2023 21:30:34 +0200 |
wenzelm |
tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
|
file |
diff |
annotate
|
| 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
|