| Tue, 02 Apr 2024 18:29:14 +0200 |
wenzelm |
clarified names: discontinue odd convention from 3 decades ago;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 14:36:29 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:10:20 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 22:40:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:38:50 +0100 |
wenzelm |
clarified signature: avoid redundant Term.maxidx_of_term;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:25:43 +0100 |
wenzelm |
proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:10:09 +0100 |
wenzelm |
misc tuning and clarification: prefer Same.operation;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 16:04:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 12:18:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:40:48 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:35:00 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 13:17:55 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 24 Dec 2023 11:51:59 +0100 |
wenzelm |
clarified modules;
|
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 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 20:22:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 20:22:58 +0200 |
wenzelm |
tuned -- avoid non-standard extend;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 14:56:55 +0200 |
wenzelm |
prefer conservative extend/merge of theory naming;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 11:17:34 +0100 |
wenzelm |
clarified signature: store full theory name;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2019 14:48:44 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2019 15:39:32 +0200 |
wenzelm |
support for a soft-type system within the Isabelle logical framework;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 09:12:13 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 18:17:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 22:31:05 +0200 |
wenzelm |
support for explicit scope of private entries;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|