src/Pure/Thy/export_theory.ML
4 weeks ago wenzelm 2019-08-15 more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
4 weeks ago wenzelm 2019-08-15 export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
4 weeks ago wenzelm 2019-08-14 uniform standard_vars for terms and proof terms;
8 weeks ago wenzelm 2019-07-21 tuned;
2 months ago wenzelm 2019-07-20 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
5 months ago wenzelm 2019-03-30 clarified signature: more explicit type Path.binding; tuned;
5 months ago wenzelm 2019-03-27 more informative Spec_Rules.Equational: support corecursion;
5 months ago wenzelm 2019-03-26 more informative Spec_Rules.Equational, notably primrec argument types;
5 months ago wenzelm 2019-03-26 export propositional status of consts;
7 months ago wenzelm 2019-02-02 clarified signature: Path.T as in Generated_Files;
11 months ago wenzelm 2018-09-30 suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
11 months ago wenzelm 2018-09-30 obsolete (see 6f8ae6ddc26b);
11 months ago wenzelm 2018-09-29 more direct locale goal: avoid renaming of type_parameters;
11 months ago wenzelm 2018-09-28 more approximative prefix syntax, including binder;
11 months ago wenzelm 2018-09-28 proper syntax for locale vs. class parameters;
11 months ago wenzelm 2018-09-26 clarified get_infix: avoid old ASCII input syntax;
11 months ago wenzelm 2018-09-25 export locale dependencies, with approx. morphism as type/term substitution;
12 months ago wenzelm 2018-09-22 obsolete (see aec64b88e708);
12 months ago wenzelm 2018-09-21 clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
12 months ago wenzelm 2018-09-21 clarified error;
12 months ago wenzelm 2018-09-21 clarified errors;
12 months ago wenzelm 2018-09-20 clarified standardization of variables, with proper treatment of local variables; tuned signature; tuned;
12 months ago wenzelm 2018-09-19 export semi-unfolded locale axioms;
12 months ago wenzelm 2018-09-16 export plain infix syntax;
12 months ago wenzelm 2018-09-15 more exports;
12 months ago wenzelm 2018-09-03 more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
12 months ago wenzelm 2018-08-31 clarified signature: proper typargs;
12 months ago wenzelm 2018-08-31 export locale content; read_theory_names: proper classrel, arities; tuned signature;
12 months ago wenzelm 2018-08-28 retain original id, which is command_id/exec_id for PIDE; tuned;
13 months ago wenzelm 2018-08-06 export shyps as regular typargs;
13 months ago wenzelm 2018-08-05 more uniform facts: single vs. multi;
13 months ago wenzelm 2018-08-05 explicit names for bound variables;
13 months ago wenzelm 2018-08-04 export in foundational order;
14 months ago wenzelm 2018-06-29 disallow hyps in export; handle extra shyps as explicit sort constraints;
15 months ago wenzelm 2018-05-26 export sort algebra;
16 months ago wenzelm 2018-05-24 more exports; read_session: proper signature;
16 months ago wenzelm 2018-05-20 standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;
16 months ago wenzelm 2018-05-20 export facts;
16 months ago wenzelm 2018-05-20 clarified encoding;
16 months ago wenzelm 2018-05-20 more scalable;
16 months ago wenzelm 2018-05-18 more exports;
16 months ago wenzelm 2018-05-17 export more theory and session structure;
16 months ago wenzelm 2018-05-17 misc tuning and clarification;
16 months ago wenzelm 2018-05-16 proper PIDE positions;
16 months ago wenzelm 2018-05-14 more general presentation hook, with document preparation as application;
16 months ago wenzelm 2018-05-13 more uniform types vs. consts;
16 months ago wenzelm 2018-05-13 more concise information;
16 months ago wenzelm 2018-05-13 clarified markup;
16 months ago wenzelm 2018-05-13 more exports; misc tuning and clarification;
16 months ago wenzelm 2018-05-11 some export of foundational theory content;