| 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
|
| Tue, 15 May 2018 17:07:41 +0200 |
wenzelm |
more uniform output (cf. 450cefec7c11);
|
file |
diff |
annotate
|
| Sat, 17 Feb 2018 12:58:07 +0100 |
wenzelm |
more informative theories_trace;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 14:11:25 +0100 |
wenzelm |
optional trace of created theory values;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 17:08:25 +0100 |
wenzelm |
auxiliary operation for space profiling;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 13:55:05 +0200 |
wenzelm |
more informative error message, e.g. relevant for incoherent imports;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 22:59:29 +0200 |
wenzelm |
proper display_name;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:43:21 +0200 |
wenzelm |
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:11:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:06:26 +0100 |
wenzelm |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:04:25 +0200 |
wenzelm |
less redundant output;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 14:16:32 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:21:25 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:48:03 +0200 |
wenzelm |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:21:04 +0200 |
wenzelm |
more abstract theory certificate, which is not necessarily the full theory;
|
file |
diff |
annotate
|