| Wed, 26 Jul 2023 11:59:55 +0200 |
wenzelm |
avoid excessive accumulation of garbage, for profiling of huge sessions;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| Thu, 11 May 2023 21:32:22 +0200 |
wenzelm |
proper position for ML-like commands;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 19:30:17 +0200 |
wenzelm |
clarified context tracing;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 15:43:49 +0200 |
wenzelm |
proper system options to control context tracing/timing;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 16:59:20 +0200 |
wenzelm |
maintain dynamic position where values are created (again, amending afa6117bace4);
|
file |
diff |
annotate
|
| Tue, 09 May 2023 16:39:08 +0200 |
wenzelm |
more robust: publish token only after assignment of result;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 16:31:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 08 May 2023 21:50:21 +0200 |
wenzelm |
more informative trace of context allocations;
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:45:58 +0200 |
wenzelm |
tuned internal structure;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2023 13:59:35 +0200 |
wenzelm |
clarified counters and types;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 21:26:35 +0200 |
wenzelm |
support n-ary merge theory data;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 15:26:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2023 23:04:26 +0200 |
wenzelm |
clarified theory_id: plain value without state;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2023 11:10:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 30 Mar 2023 16:10:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 21:48:47 +0200 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
| Mon, 20 Mar 2023 11:09:51 +0100 |
wenzelm |
clarified theory_sizeof1_data: count bytes, individually for each data entry;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2021 12:09:15 +0200 |
wenzelm |
more exports, notably for Isabelle/Naproche;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2020 23:45:29 +0200 |
wenzelm |
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 12:58:53 +0200 |
wenzelm |
maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
|
file |
diff |
annotate
|
| Thu, 01 Aug 2019 09:50:20 +0200 |
wenzelm |
abstract type theory_id -- ensure non-equality type independently of implementation;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2019 12:31:24 +0200 |
wenzelm |
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2019 11:26:00 +0200 |
wenzelm |
clarified history stage: allow independent updates that are merged later;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2018 14:49:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 16 May 2018 15:18:12 +0200 |
wenzelm |
more thorough checks for theory name consistency (for extend, not just merge);
|
file |
diff |
annotate
|