| 5 months ago |
wenzelm |
clarified signature: uniform context;
|
file |
diff |
annotate
|
| 5 months ago |
wenzelm |
proper context for extern operation: observe local options;
|
file |
diff |
annotate
|
| 9 months ago |
wenzelm |
clarified thm_header command_pos vs. thm_pos;
|
file |
diff |
annotate
|
| 11 months ago |
wenzelm |
more accurate thm "name_hint", using Thm_Name.T;
|
file |
diff |
annotate
|
| 11 months ago |
wenzelm |
more accurate output of Thm_Name.T wrt. facts name space;
|
file |
diff |
annotate
|
| 11 months ago |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned: avoid duplicates;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
proper Thm_Name.make_list for thm_definition;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
unused;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
proper thm_name for stored zproof;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
uniform treatment of lazy facts: actual proof terms are always strict;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 17 months ago |
wenzelm |
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
|
file |
diff |
annotate
|
| 17 months ago |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| 17 months ago |
wenzelm |
pro-forma support for optional zproof: no proper content yet;
|
file |
diff |
annotate
|
| 2023-05-06 |
wenzelm |
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
|
file |
diff |
annotate
|
| 2023-05-05 |
wenzelm |
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
|
file |
diff |
annotate
|
| 2023-04-20 |
wenzelm |
proper theory_long_name;
|
file |
diff |
annotate
|
| 2023-04-20 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| 2021-10-20 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| 2021-09-07 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| 2021-09-04 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2020-08-06 |
wenzelm |
more robust treatment of thm_names, with strict check after all theories are loaded;
|
file |
diff |
annotate
|
| 2020-07-17 |
wenzelm |
clarified -- avoid non-standard extend;
|
file |
diff |
annotate
|
| 2019-11-04 |
wenzelm |
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
|
file |
diff |
annotate
|
| 2019-11-02 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2019-11-01 |
wenzelm |
proper export of unnamed proof boxes for unnamed toplevel declarations, e.g. rulify/defn rules in theory IFOL and HOL;
|
file |
diff |
annotate
|
| 2019-10-18 |
wenzelm |
proper treatment of self thm_id;
|
file |
diff |
annotate
|
| 2019-10-17 |
wenzelm |
proper Thm.transfer;
|
file |
diff |
annotate
|
| 2019-08-20 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2019-08-19 |
wenzelm |
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
|
file |
diff |
annotate
|
| 2019-08-19 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2019-08-17 |
wenzelm |
clarified lookup operations: more scalable for multiple retrieval;
|
file |
diff |
annotate
|
| 2019-08-16 |
wenzelm |
maintain thm_name vs. derivation_id for global facts;
|
file |
diff |
annotate
|
| 2019-08-16 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2019-08-16 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2019-08-16 |
wenzelm |
clarified derivation_name vs. raw_derivation_name;
|
file |
diff |
annotate
|
| 2019-08-09 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| 2019-08-03 |
wenzelm |
maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
|
file |
diff |
annotate
|
| 2019-07-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2019-07-28 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2019-07-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2019-07-28 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|