Sun, 14 Jul 2024 17:49:30 +0200 |
wenzelm |
clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;
|
file |
diff |
annotate
|
Sun, 09 Jun 2024 21:16:38 +0200 |
wenzelm |
clarified data representation: prefer explicit type Thm_Name;
|
file |
diff |
annotate
|
Fri, 07 Jun 2024 23:53:31 +0200 |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
file |
diff |
annotate
|
Fri, 24 Feb 2023 20:40:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 21 Oct 2022 16:39:31 +0200 |
wenzelm |
generic support for XZ and Zstd compression in Isabelle/Scala;
|
file |
diff |
annotate
|
Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
Mon, 08 Nov 2021 12:45:35 +0100 |
wenzelm |
just one cache, via HTML_Context, via Sessions.Store or Session;
|
file |
diff |
annotate
|
Wed, 04 Aug 2021 22:20:47 +0200 |
wenzelm |
prefer persistent hash code for cachable items (see also 72b13af7f266);
|
file |
diff |
annotate
|
Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
Sat, 02 Jan 2021 16:09:45 +0100 |
wenzelm |
more uniform default --- hardly relevant in practice;
|
file |
diff |
annotate
|
Sat, 02 Jan 2021 15:58:48 +0100 |
wenzelm |
clarified signature --- internal Cache.none;
|
file |
diff |
annotate
|
Wed, 22 Apr 2020 17:52:14 +0200 |
wenzelm |
tuned signature -- avoid warnings;
|
file |
diff |
annotate
|
Tue, 21 Apr 2020 22:19:59 +0200 |
wenzelm |
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
|
file |
diff |
annotate
|
Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
Tue, 03 Dec 2019 15:59:01 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
Sun, 20 Oct 2019 21:12:18 +0200 |
wenzelm |
clarified signature: name of standard_proof is authentic, otherwise empty;
|
file |
diff |
annotate
|
Thu, 17 Oct 2019 21:31:53 +0200 |
wenzelm |
support dummy term;
|
file |
diff |
annotate
|
Sat, 12 Oct 2019 22:20:39 +0200 |
wenzelm |
clarified signature default;
|
file |
diff |
annotate
|
Sat, 12 Oct 2019 22:18:27 +0200 |
wenzelm |
clarified signature default;
|
file |
diff |
annotate
|
Sat, 12 Oct 2019 22:12:29 +0200 |
wenzelm |
more operations for type classes;
|
file |
diff |
annotate
|
Sat, 12 Oct 2019 15:41:59 +0200 |
wenzelm |
clarified output and input of Typ/Term;
|
file |
diff |
annotate
|
Fri, 11 Oct 2019 18:26:35 +0200 |
wenzelm |
clarified oracle_proof;
|
file |
diff |
annotate
|
Fri, 04 Oct 2019 16:34:14 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
Fri, 04 Oct 2019 15:30:52 +0200 |
wenzelm |
Term_XML.Encode/Decode.term uses Const "typargs";
|
file |
diff |
annotate
|
Sat, 17 Aug 2019 11:52:47 +0200 |
wenzelm |
clarified type for recorded oracles;
|
file |
diff |
annotate
|
Sat, 17 Aug 2019 10:38:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 16:57:09 +0200 |
wenzelm |
clarified PThm: theory_name simplifies retrieval from exports;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 16:38:55 +0200 |
wenzelm |
Indexname.toString according to string_of_vname' in ML;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 16:26:50 +0200 |
wenzelm |
clarified type Indexname, with plain value Int;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 16:17:18 +0200 |
wenzelm |
more complete pattern match;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 16:02:47 +0200 |
wenzelm |
support for (fully reconstructed) proof terms in Scala;
|
file |
diff |
annotate
|
Sat, 20 Jul 2019 14:03:51 +0200 |
wenzelm |
more operations: support type classes within the logic;
|
file |
diff |
annotate
|
Sat, 20 Jul 2019 11:48:30 +0200 |
wenzelm |
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
|
file |
diff |
annotate
|
Thu, 24 May 2018 21:13:09 +0200 |
wenzelm |
more general cache, also for term substructures;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 18:00:05 +0200 |
wenzelm |
more uniform Term and Term_XML modules;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 17:53:06 +0200 |
wenzelm |
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 10:44:30 +0200 |
wenzelm |
tuned XML modules;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 17:58:11 +0200 |
wenzelm |
lambda terms with XML data representation in Scala;
|
file |
diff |
annotate
|