Code_Runtime.value, corresponding to ML_Context.value

more accurate dependencies

code_eval renamed to code_runtime

merged

static nbe conversion

ignore code cache optionally; corrected scope of term value in static_eval_conv

ignore code cache optionally

dropped redundant normal_form command

more explicit theory name

more accurate dependencies

merged

more clear separation of static compilation and dynamic evaluation

Document.async_state: some attempts to make this more robust wrt. cancelation of the main transaction -- avoid confusing feedback about pending forks;

isatest: reactivated kodkodi and thus HOL-Nitpick_Examples -- being now on a local file system greatly increases the chance that it works;

merged

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures

merge

compile on SML/NJ

in debug mode, don't touch "$true" and "$false"

adding option show_invalid_clauses for a more detailed message when modes are not inferred

proposed modes for code_pred now supports modes for mutual predicates

merged

established emerging canonical names *_eqI and *_eq_iff

moved lemmas map_of_eqI and map_of_eq_dom to Map.thy

more precise name for activation of improveable syntax

tuning

tuning