make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice

added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice

compute quantifier dependency graph in new skolemizer

tuning

compute substitutions in new skolemizer

encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions

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";