Sun, 14 Aug 2022 11:20:10 +0200 |
wenzelm |
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
|
file |
diff |
annotate
|
Fri, 05 Aug 2022 14:05:42 +0200 |
wenzelm |
more uniform exports: proper encoding of empty parents for Pure;
|
file |
diff |
annotate
|
Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
Wed, 08 Sep 2021 08:41:36 +0200 |
wenzelm |
simplified: uniqueness check happens in export_consumer;
|
file |
diff |
annotate
|
Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Wed, 04 Aug 2021 19:41:59 +0200 |
wenzelm |
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
|
file |
diff |
annotate
|
Tue, 24 Mar 2020 13:43:29 +0100 |
wenzelm |
avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;
|
file |
diff |
annotate
|
Fri, 06 Dec 2019 15:53:09 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 03 Dec 2019 16:40:04 +0100 |
wenzelm |
clarified export of consts: recursion is accessible via spec_rules;
|
file |
diff |
annotate
|
Tue, 03 Dec 2019 10:50:28 +0100 |
wenzelm |
clarified position for spec rule: like entity;
|
file |
diff |
annotate
|
Mon, 02 Dec 2019 15:30:17 +0100 |
wenzelm |
proper treatment of variable names;
|
file |
diff |
annotate
|
Mon, 02 Dec 2019 13:03:09 +0100 |
wenzelm |
more informative export;
|
file |
diff |
annotate
|
Mon, 02 Dec 2019 12:03:55 +0100 |
wenzelm |
tuned signature -- following Export_Theory.Spec_Rule in Scala;
|
file |
diff |
annotate
|
Mon, 02 Dec 2019 11:57:53 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
Mon, 02 Dec 2019 11:57:42 +0100 |
wenzelm |
clarified export of spec rules: more like locale;
|
file |
diff |
annotate
|
Sun, 01 Dec 2019 21:29:08 +0100 |
wenzelm |
formal position for spec rule (not significant for equality);
|
file |
diff |
annotate
|
Sat, 30 Nov 2019 15:17:23 +0100 |
wenzelm |
export spec rules;
|
file |
diff |
annotate
|
Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
file |
diff |
annotate
|
Fri, 08 Nov 2019 19:06:50 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 14:56:49 +0100 |
wenzelm |
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
|
file |
diff |
annotate
|
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
|
Sat, 02 Nov 2019 12:33:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 12:11:00 +0100 |
wenzelm |
more direct output of XML material -- bypass Buffer.T;
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 12:02:27 +0100 |
wenzelm |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 10:56:53 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 01 Nov 2019 18:08:46 +0100 |
wenzelm |
clarified signature (again);
|
file |
diff |
annotate
|
Fri, 01 Nov 2019 17:53:27 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 01 Nov 2019 15:47:31 +0100 |
wenzelm |
avoid redundant proof boxes for application sessions;
|
file |
diff |
annotate
|
Fri, 01 Nov 2019 15:09:55 +0100 |
wenzelm |
more detailed proof term output;
|
file |
diff |
annotate
|
Thu, 31 Oct 2019 22:34:16 +0100 |
wenzelm |
more accurate proof_boxes -- from actual proof body;
|
file |
diff |
annotate
|
Thu, 31 Oct 2019 21:21:09 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 31 Oct 2019 14:29:29 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Tue, 22 Oct 2019 20:55:13 +0200 |
wenzelm |
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
|
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 22:26:44 +0200 |
wenzelm |
avoid spurious shyps (with vacous type variable);
|
file |
diff |
annotate
|
Sun, 20 Oct 2019 21:34:29 +0200 |
wenzelm |
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
|
file |
diff |
annotate
|
Sun, 20 Oct 2019 20:38:22 +0200 |
wenzelm |
clarified expand_proof/expand_name: allow more detailed control via thm_header;
|
file |
diff |
annotate
|
Sun, 20 Oct 2019 16:16:23 +0200 |
wenzelm |
option to export standardized proof terms (not scalable);
|
file |
diff |
annotate
|
Sat, 19 Oct 2019 16:09:39 +0200 |
wenzelm |
export toplevel proof similar to named PThm;
|
file |
diff |
annotate
|
Fri, 18 Oct 2019 22:44:19 +0200 |
wenzelm |
proper treatment of self thm_id;
|
file |
diff |
annotate
|
Thu, 17 Oct 2019 21:03:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 17 Oct 2019 20:56:18 +0200 |
wenzelm |
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
|
file |
diff |
annotate
|
Thu, 17 Oct 2019 17:24:13 +0200 |
wenzelm |
clarified proof_boxes (requires prune_proofs=false);
|
file |
diff |
annotate
|
Tue, 15 Oct 2019 21:05:35 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
Sat, 12 Oct 2019 13:43:17 +0200 |
wenzelm |
more compact XML: separate environment for free variables;
|
file |
diff |
annotate
|
Fri, 11 Oct 2019 11:16:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 04 Oct 2019 15:30:52 +0200 |
wenzelm |
Term_XML.Encode/Decode.term uses Const "typargs";
|
file |
diff |
annotate
|
Fri, 23 Aug 2019 14:32:51 +0200 |
wenzelm |
clarified 'thm_deps' command;
|
file |
diff |
annotate
|
Fri, 23 Aug 2019 13:32:27 +0200 |
wenzelm |
more compact: avoid pointless PThm rudiments;
|
file |
diff |
annotate
|
Wed, 21 Aug 2019 17:32:44 +0200 |
wenzelm |
more scalable: avoid huge intermediate XML elems;
|
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 21:18:06 +0200 |
wenzelm |
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
|
file |
diff |
annotate
|
Thu, 15 Aug 2019 19:35:17 +0200 |
wenzelm |
more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
|
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
|
Wed, 14 Aug 2019 19:21:34 +0200 |
wenzelm |
uniform standard_vars for terms and proof terms;
|
file |
diff |
annotate
|
Sun, 21 Jul 2019 12:11:35 +0200 |
wenzelm |
tuned;
|
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
|
Sat, 30 Mar 2019 20:54:47 +0100 |
wenzelm |
clarified signature: more explicit type Path.binding;
|
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
|
Sat, 02 Feb 2019 15:52:14 +0100 |
wenzelm |
clarified signature: Path.T as in Generated_Files;
|
file |
diff |
annotate
|
Sun, 30 Sep 2018 12:26:14 +0200 |
wenzelm |
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
|
file |
diff |
annotate
|
Sun, 30 Sep 2018 11:58:59 +0200 |
wenzelm |
obsolete (see 6f8ae6ddc26b);
|
file |
diff |
annotate
|
Sat, 29 Sep 2018 23:23:43 +0200 |
wenzelm |
more direct locale goal: avoid renaming of type_parameters;
|
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
|
Wed, 26 Sep 2018 17:04:50 +0200 |
wenzelm |
clarified get_infix: avoid old ASCII input syntax;
|
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
|
Sat, 22 Sep 2018 15:22:29 +0200 |
wenzelm |
obsolete (see aec64b88e708);
|
file |
diff |
annotate
|
Fri, 21 Sep 2018 22:26:10 +0200 |
wenzelm |
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
|
file |
diff |
annotate
|
Fri, 21 Sep 2018 21:06:23 +0200 |
wenzelm |
clarified error;
|
file |
diff |
annotate
|
Fri, 21 Sep 2018 17:48:39 +0200 |
wenzelm |
clarified errors;
|
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
|
Mon, 03 Sep 2018 20:46:09 +0200 |
wenzelm |
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of 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 12:07:30 +0200 |
wenzelm |
retain original id, which is command_id/exec_id for PIDE;
|
file |
diff |
annotate
|
Mon, 06 Aug 2018 11:06:43 +0200 |
wenzelm |
export shyps as regular typargs;
|
file |
diff |
annotate
|
Sun, 05 Aug 2018 20:32:18 +0200 |
wenzelm |
more uniform facts: single vs. multi;
|
file |
diff |
annotate
|
Sun, 05 Aug 2018 14:50:11 +0200 |
wenzelm |
explicit names for bound variables;
|
file |
diff |
annotate
|
Sat, 04 Aug 2018 22:32:41 +0200 |
wenzelm |
export in foundational order;
|
file |
diff |
annotate
|
Fri, 29 Jun 2018 14:19:52 +0200 |
wenzelm |
disallow hyps in export;
|
file |
diff |
annotate
|
Sat, 26 May 2018 22:02:25 +0200 |
wenzelm |
export sort algebra;
|
file |
diff |
annotate
|
Thu, 24 May 2018 16:56:14 +0200 |
wenzelm |
more exports;
|
file |
diff |
annotate
|
Sun, 20 May 2018 20:37:11 +0200 |
wenzelm |
standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;
|
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
|
Sun, 20 May 2018 15:28:59 +0200 |
wenzelm |
more scalable;
|
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:01:13 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
Wed, 16 May 2018 23:13:33 +0200 |
wenzelm |
proper PIDE positions;
|
file |
diff |
annotate
|
Mon, 14 May 2018 11:29:22 +0200 |
wenzelm |
more general presentation hook, with document preparation as application;
|
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 16:51:50 +0200 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
Sun, 13 May 2018 15:55:30 +0200 |
wenzelm |
more exports;
|
file |
diff |
annotate
|
Fri, 11 May 2018 22:59:00 +0200 |
wenzelm |
some export of foundational theory content;
|
file |
diff |
annotate
|