| Sun, 03 Nov 2019 18:55:35 +0100 |
wenzelm |
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
|
file |
diff |
annotate
|
| Mon, 21 Oct 2019 16:32:10 +0200 |
wenzelm |
export constdefs according to defs.ML;
|
file |
diff |
annotate
|
| Sun, 20 Oct 2019 12:56:36 +0200 |
wenzelm |
more kinds, notably for Isabelle/MMT;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 16:25:54 +0200 |
wenzelm |
clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 21:03:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 16:10:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 14:06:14 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 21:05:35 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:41:47 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:04:11 +0200 |
wenzelm |
support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 14:14:10 +0200 |
wenzelm |
clarified proof export;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 13:43:17 +0200 |
wenzelm |
more compact XML: separate environment for free variables;
|
file |
diff |
annotate
|
| Sun, 06 Oct 2019 16:22:43 +0200 |
wenzelm |
clarified signature: read full session requirements;
|
file |
diff |
annotate
|
| Sun, 06 Oct 2019 15:28:59 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 19:56:31 +0200 |
wenzelm |
export thm_deps;
|
file |
diff |
annotate
|
| Mon, 19 Aug 2019 21:23:13 +0200 |
wenzelm |
clarified export of axioms and theorems (identified derivations instead of projected facts);
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 18:21:12 +0200 |
wenzelm |
support Export_Theory.read_proof, based on theory_name and serial;
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:06:57 +0200 |
wenzelm |
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2019 12:52:29 +0200 |
wenzelm |
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2019 14:47:49 +0100 |
wenzelm |
more informative Spec_Rules.Equational: support corecursion;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 22:13:36 +0100 |
wenzelm |
more informative Spec_Rules.Equational, notably primrec argument types;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 13:25:32 +0100 |
wenzelm |
export propositional status of consts;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 21:16:24 +0200 |
wenzelm |
more approximative prefix syntax, including binder;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 19:30:07 +0200 |
wenzelm |
proper syntax for locale vs. class parameters;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2018 20:41:27 +0200 |
wenzelm |
export locale dependencies, with approx. morphism as type/term substitution;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 22:39:39 +0200 |
wenzelm |
clarified standardization of variables, with proper treatment of local variables;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2018 22:18:36 +0200 |
wenzelm |
export semi-unfolded locale axioms;
|
file |
diff |
annotate
|
| Sun, 16 Sep 2018 22:45:34 +0200 |
wenzelm |
export plain infix syntax;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2018 23:35:46 +0200 |
wenzelm |
more exports;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2018 16:17:30 +0200 |
wenzelm |
clarified signature: proper typargs;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2018 15:48:37 +0200 |
wenzelm |
export locale content;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 15:25:28 +0200 |
wenzelm |
more robust: Pure entities may lack id;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 12:07:30 +0200 |
wenzelm |
retain original id, which is command_id/exec_id for PIDE;
|
file |
diff |
annotate
|
| Sun, 05 Aug 2018 20:32:18 +0200 |
wenzelm |
more uniform facts: single vs. multi;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2018 21:38:54 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2018 20:14:13 +0200 |
wenzelm |
tuned signature -- removed somewhat pointless operation;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2018 15:29:18 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Fri, 03 Aug 2018 15:04:24 +0200 |
wenzelm |
more explicit entity kind;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2018 22:24:16 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2018 21:49:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2018 14:21:48 +0200 |
wenzelm |
always export Pure theory;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2018 18:05:43 +0200 |
wenzelm |
more abstract Export.Provider;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2018 11:50:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 26 May 2018 22:02:25 +0200 |
wenzelm |
export sort algebra;
|
file |
diff |
annotate
|
| Thu, 24 May 2018 21:36:39 +0200 |
wenzelm |
more scalable JVM memory management;
|
file |
diff |
annotate
|
| Thu, 24 May 2018 16:56:14 +0200 |
wenzelm |
more exports;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 16:25:27 +0200 |
wenzelm |
export facts;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 15:37:16 +0200 |
wenzelm |
clarified encoding;
|
file |
diff |
annotate
|
| Sat, 19 May 2018 20:19:15 +0200 |
wenzelm |
tuned queries;
|
file |
diff |
annotate
|
| Fri, 18 May 2018 17:21:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 18 May 2018 17:09:55 +0200 |
wenzelm |
support Store with options;
|
file |
diff |
annotate
|
| Fri, 18 May 2018 16:30:20 +0200 |
wenzelm |
more exports;
|
file |
diff |
annotate
|
| Thu, 17 May 2018 17:29:17 +0200 |
wenzelm |
export more theory and session structure;
|
file |
diff |
annotate
|
| Thu, 17 May 2018 14:50:48 +0200 |
wenzelm |
read theory content from session database;
|
file |
diff |
annotate
|
| Sun, 13 May 2018 21:20:28 +0200 |
wenzelm |
more uniform types vs. consts;
|
file |
diff |
annotate
|
| Sun, 13 May 2018 20:24:33 +0200 |
wenzelm |
more concise information;
|
file |
diff |
annotate
|
| Sun, 13 May 2018 20:04:59 +0200 |
wenzelm |
export foundational theory content in Scala;
|
file |
diff |
annotate
|