reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer

encode number of skolem assumptions in them, for more efficient retrieval later

move functions closer to where they're used

Skolemizer tweaking

"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))

finished renaming file and module

rename file

ignore Skolem assumption (if any)

second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions

first step towards a new skolemizer that doesn't require "Eps"

cumulative update of generated files (since bf164c153d10);

removed ML_old.thy, which is largely superseded by ML.thy;

more on "Canonical argument order"; tuned;

cover @{Isar.state};

more on "Style and orthography";

more on "Naming conventions"; tuned;

tuned;

more on "Style and orthography";

more refs;

preliminary material on "Concrete syntax and type-checking";

more on "Association lists", based on more succinct version of older material;

clarified "lists as a set-like container";

more robust treatment of "op IDENT";

more on messages;

more on synchronized variables;

tuned;

more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);

misc tuning;

somewhat modernized version of "Thread-safe programming";

more robust examples: explicit @{assert} instead of unchecked output;