| 7 months ago |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
more compact representation of theory_id -- via consecutive thread-local ids;
|
file |
diff |
annotate
|
| 16 months ago |
wenzelm |
more compact representation of theory_id;
|
file |
diff |
annotate
|
| 20 months ago |
wenzelm |
avoid excessive accumulation of garbage, for profiling of huge sessions;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
proper position for ML-like commands;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
clarified context tracing;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
proper system options to control context tracing/timing;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
maintain dynamic position where values are created (again, amending afa6117bace4);
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
more robust: publish token only after assignment of result;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
more informative trace of context allocations;
|
file |
diff |
annotate
|
| 23 months ago |
wenzelm |
tuned internal structure;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
clarified counters and types;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
support n-ary merge theory data;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
clarified theory_id: plain value without state;
|
file |
diff |
annotate
|
| 24 months ago |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2023-03-30 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2023-03-27 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
| 2023-03-20 |
wenzelm |
clarified theory_sizeof1_data: count bytes, individually for each data entry;
|
file |
diff |
annotate
|
| 2021-10-20 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| 2021-10-05 |
wenzelm |
more exports, notably for Isabelle/Naproche;
|
file |
diff |
annotate
|
| 2021-09-04 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2020-07-20 |
wenzelm |
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
|
file |
diff |
annotate
|
| 2019-08-20 |
wenzelm |
clarified signature;
|
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-08-01 |
wenzelm |
abstract type theory_id -- ensure non-equality type independently of implementation;
|
file |
diff |
annotate
|
| 2019-07-04 |
wenzelm |
support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
|
file |
diff |
annotate
|
| 2019-07-04 |
wenzelm |
clarified history stage: allow independent updates that are merged later;
|
file |
diff |
annotate
|
| 2018-06-21 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 2018-05-16 |
wenzelm |
more thorough checks for theory name consistency (for extend, not just merge);
|
file |
diff |
annotate
|
| 2018-05-15 |
wenzelm |
more uniform output (cf. 450cefec7c11);
|
file |
diff |
annotate
|
| 2018-02-17 |
wenzelm |
more informative theories_trace;
|
file |
diff |
annotate
|
| 2018-02-16 |
wenzelm |
optional trace of created theory values;
|
file |
diff |
annotate
|
| 2018-02-15 |
wenzelm |
auxiliary operation for space profiling;
|
file |
diff |
annotate
|
| 2017-08-18 |
wenzelm |
more informative error message, e.g. relevant for incoherent imports;
|
file |
diff |
annotate
|
| 2017-04-10 |
wenzelm |
proper display_name;
|
file |
diff |
annotate
|
| 2017-04-10 |
wenzelm |
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
|
file |
diff |
annotate
|
| 2016-04-06 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2016-04-05 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| 2016-04-02 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| 2016-03-18 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| 2015-12-20 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-12-20 |
wenzelm |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
less redundant output;
|
file |
diff |
annotate
|
| 2015-09-25 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| 2015-08-31 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| 2015-08-30 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| 2015-08-28 |
wenzelm |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
file |
diff |
annotate
|
| 2015-08-28 |
wenzelm |
more abstract theory certificate, which is not necessarily the full theory;
|
file |
diff |
annotate
|
| 2015-08-16 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| 2015-08-16 |
wenzelm |
separate type theory_id;
|
file |
diff |
annotate
|
| 2014-12-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2014-12-18 |
wenzelm |
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
|
file |
diff |
annotate
|
| 2014-11-26 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| 2014-02-17 |
wenzelm |
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
|
file |
diff |
annotate
|
| 2013-07-30 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| 2013-07-18 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
file |
diff |
annotate
|