tuned signature;

tuned;

more accurate Thm.trim_context / Thm.transfer;

tuned signature;

tuned whitespace;

update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;

clarified signature: avoid convoluted operations;

avoid capture of inner/outer context and thus reduce heaps sizes by 20..40%…

proper transfer / trim_context;

more operations "without_context", assuming that the thm has been properly…

tuned: more accurate check (is_norm_hhf protect);

proper trim_context / transfer;

more standard merge order, following logical structure of imports rather than…

clarified build options: reduce heap size by approx. 3%;

tuned;

tuned;

proper Thm.trim_context / Thm.transfer;

tuned: avoid pointless Proof_Context.init_global of Context.proof_of;

proper Thm.trim_context / Thm.transfer;

merged

SMT-LIB interpretation of floating-point arithmetic

SMT-LIB interpretation of floating-point arithmetic

Minor

IEEE model with a single NaN value

New material from the HOL Light metric space library, mostly about quasi…

More material from the HOL Light metric space library

merging

updates for future formalizations

proper Thm.trim_context / Thm.transfer;

proper position for ML-like commands;

adapted to Isabelle/f78cdc6fe971;

adapted to Isabelle/f78cdc6fe971;

Reset the save-vec after calls to the objsize function. Includes regression…

A slight beautification

more robust: after shutdown;

proper exception CONTEXT for Context.certificate_theory;

more diagnostic operations;

more standard treatment of data and context;

tuned spelling;

tuned;

more standard val silent = Attrib.setup_config_bool;

adapted to 3f354d5bbf98;

tuned;

proper Thm.trim_context / Thm.transfer;

proper Thm.trim_context / Thm.transfer;

tuned Isabelle/ML;

more informative position information;

tuned;

clarified context tracing;

more informative position information;

more operations;

proper system options to control context tracing/timing;

Rounding modes renamed

merged

Add the rounding mode roundNearestTiesToAway.

added lemmas transp_on_multpHO and transp_multpHO

tuned theory structure

merged

added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered…

backed out changeset 6c2494750a4e: it hardly makes a difference for heap size…

enforce rebuild of Isabelle/ML + Isabelle/Scala;

updated to jdk-17.0.7;

performance tuning: cached non-persistent Parser.gram reduces heap size by…

more operations;

minor performance tuning (see also f906f7f83dae and b23c42b9f78a);

tuned;

tuned: more readable ML;

backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);

maintain dynamic position where values are created (again, amending…

more robust: publish token only after assignment of result;

tuned comments;

clarified signature;

merged

tuned signature;

support for cached evaluation via weak_ref;

more informative trace of context allocations;

optional timing;

tuned;

tuned internal structure;

tuned;

tuned whitespace;

Merge realtime deque renamings

simplify some measurements

rename Deque.Idle to Idles

Rename Big and Small cases

rename `Transforming` to `Rebal`

rename `Common.state` to `common_state`

merged

added lemma asymp_on_multpHO

added author

added lemmas count_minus_inter_lt_count_minus_inter_iff and…

added lemmas multpHO_iff_set_mset_lessHO_set_mset and…

added lemma multpHO_implies_one_step_strong

rename Small.state to small_state

rename Big.state to big_state

backed out changeset 2ecb8f5e085f: obsolete thanks to Isabelle/21cdcd120a78;

more robust: make it work with Isabelle/a12c48fbf10f;