| Thu, 15 Aug 2024 13:45:48 +0200 |
wenzelm |
provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;
|
file |
diff |
annotate
|
| Thu, 15 Aug 2024 12:43:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 15 Aug 2024 12:22:39 +0200 |
wenzelm |
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
|
file |
diff |
annotate
|
| Thu, 15 Aug 2024 11:49:45 +0200 |
wenzelm |
tuned;
|
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
|
| Wed, 14 Aug 2024 16:48:16 +0200 |
wenzelm |
tuned: anticipate congprocs;
|
file |
diff |
annotate
|
| Wed, 14 Aug 2024 15:30:29 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 14 Aug 2024 13:51:36 +0200 |
wenzelm |
tuned signature (again): anticipate different kinds of procs;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 18:31:40 +0200 |
wenzelm |
clarified signature: less redundant types;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 16:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 15:50:25 +0200 |
wenzelm |
unused (see d12c58e12c51);
|
file |
diff |
annotate
|
| Tue, 13 Aug 2024 15:42:55 +0200 |
wenzelm |
tuned signature: support more general procedures;
|
file |
diff |
annotate
|
| Sun, 09 Jun 2024 15:31:33 +0200 |
wenzelm |
more accurate thm "name_hint", using Thm_Name.T;
|
file |
diff |
annotate
|
| Sun, 09 Jun 2024 12:29:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 01 Apr 2024 15:47:15 +0200 |
wenzelm |
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
|
file |
diff |
annotate
|
| Mon, 01 Apr 2024 15:37:55 +0200 |
wenzelm |
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
|
file |
diff |
annotate
|
| Tue, 27 Feb 2024 17:06:19 +0100 |
nipkow |
tuned name
|
file |
diff |
annotate
|
| Tue, 27 Feb 2024 11:59:47 +0100 |
nipkow |
new simplifier trace_op for tracing simproc calls
|
file |
diff |
annotate
|
| Tue, 27 Feb 2024 10:49:48 +0100 |
nipkow |
simplifier: no trace info from simprocs unless simp_debug = true.
|
file |
diff |
annotate
|
| Sun, 22 Oct 2023 13:56:52 +0200 |
wenzelm |
tuned;
|
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
|
| Thu, 19 Oct 2023 17:06:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2023 14:12:26 +0200 |
wenzelm |
performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 11:33:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 May 2023 13:19:49 +0200 |
wenzelm |
clarified treatment of context;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 16:12:37 +0200 |
wenzelm |
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
|
file |
diff |
annotate
|
| Fri, 19 May 2023 21:22:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 19 May 2023 11:41:30 +0200 |
wenzelm |
more careful reset_context for stored entity;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 14:09:45 +0200 |
wenzelm |
more operations "without_context", assuming that the thm has been properly transferred already;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 10:59:49 +0200 |
wenzelm |
tuned: more accurate check (is_norm_hhf protect);
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2023 23:32:46 +0200 |
wenzelm |
revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 22:38:18 +0200 |
wenzelm |
performance tuning: replace Ord_List by Set();
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Thu, 14 Oct 2021 16:03:20 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 13 Oct 2021 13:19:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 13:49:26 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2020 19:17:59 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 19 Dec 2019 15:29:48 +0100 |
wenzelm |
proper proof body context for Simplifier plugins (solvers, loopers, ...) -- avoid crash due to Subgoal.FOCUS (before e58bc223f46c);
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 12:09:35 +0000 |
haftmann |
proper table data structure
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 09:24:34 +0000 |
haftmann |
more direct accessors for simpset
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 20:25:21 +0000 |
haftmann |
regular merge with no historization, in accordance with regular update
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:13:23 +0100 |
wenzelm |
more structural integrity;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 14 Aug 2019 11:14:27 +0200 |
wenzelm |
treat simproc results as atomic -- more compact proof terms;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2018 17:12:28 +0200 |
Lars Hupel |
Jenkins: run ocaml_setup
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 15:08:18 +0200 |
nipkow |
comments
|
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
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:31:25 +0100 |
wenzelm |
clarified signature: prefer proper order operation;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2017 07:46:28 +0100 |
nipkow |
reduced simp_depth_limit
|
file |
diff |
annotate
|