| Mon, 02 Dec 2024 22:16:29 +0100 |
wenzelm |
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 19:21:38 +0100 |
wenzelm |
eliminate historic clone (see also 550e36c6a2d1);
|
file |
diff |
annotate
|
| Wed, 14 Aug 2024 21:23:22 +0200 |
wenzelm |
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 21:09:51 +0200 |
wenzelm |
tuned: prefer canonical argument order;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2024 14:44:51 +0200 |
wenzelm |
tuned signature: eliminate aliases;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 17:39:47 +0200 |
wenzelm |
tuned: more explicit dest_Const_name and dest_Const_type;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
file |
diff |
annotate
|
| 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 00:13:12 +0200 |
wenzelm |
more standard simproc_setup using ML antiquotation;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 19:12:21 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 17:45:47 +0200 |
wenzelm |
more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 13:41:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 01:44:52 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 20:49:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 05 Apr 2017 19:23:41 +0200 |
Lars Hupel |
use Item_Net to store inductive info
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 20:56:44 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 11:03:02 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 09:40:04 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|