document Metis updating procedure

move "CRITICAL" to "PortableXxx", where it belongs and used to be; now that it is no longer used in "Random.sml"

regenerated "metis.ML"

update comment

make "Unprotected concurrency introduces some true randomness." be true; this code is called often and doesn't need to be considered critical. I added CRITICAL by mistake.

fix parsing of higher-order formulas; this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively

merged

load code_runtime immediately again

proper interface for code_reflect

introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy

merged

"Metis." -> "Metis_" to reflect change in "metis.ML"

no need for "metis_env.ML" anymore; it was a neat solution but it didn't work anymore once I removed the "structure Metis"

regenerate "metis.ML", this time without manual hacks

remove needless file for us

got rid of three crude regexps from "make_metis"

more Isabelle-specific changes

tuning

rename

use "Metis_" prefix rather than "Metis" structure; the prefix can then be used not only for structures but also signatures and functors. A few other changes were made to the script, to eliminate the need for "metis_env.ML".

no need for TPTP

put "foldl" and "foldr" in "Useful"; Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix

reintroduce the CRITICAL sections from change 3880d21d6013

apply Larry's hacks directly to the "src" files; these hacks modify the defaults of Metis heuristics and are necessary for backward compatibility

"FILES" is not (anymore?) part of the official Metis sources, so move it up

merged

Code_Runtime.value, corresponding to ML_Context.value; tuned

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

prefer version 0.6 of Vampire, now that we can parse its output

fix splitting of proof lines for one-line metis calls; needed for newly supported ATPs (Vampire 0.6 local and remote, SNARK)

finish support for E 1.2 proof reconstruction; this involves picking up the axiom and conjecture names specified using a "file" annotation in the TSTP file, since we cannot rely anymore on formula numbers (E 1.2 adds a strange offset)

first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)

clarify message