merged

qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)

get rid of function that duplicates existing Pure functionality

remove needless fact

added a few FIXMEs

tuned comments

document latest changes to Meson/Metis/Sledgehammer

remove needless Metis facts

hide one more name

qualify names

hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names

clean up debugging output

factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

got rid of overkill "meson_choice" attribute; tuning

more explicit name

factor out "Meson_Tactic" from "Meson_Clausify"

tuning

move Metis into Plain

added "Meson" theory to Makefile

update authors

remove Meson from Hilbert_Choice

remove Meson from Sledgehammer

move Meson to Plain

move MESON files together

paramify new skolems just like old ones (cf. reveal_old_skolem_terms)

fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset

correctly handle multiple copies of the same axiom with the same types

put two operations in the right order

reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism

apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed

instantiate foralls and release exists in the order described by the topological order

reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables

renamed internal function

hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving

tuned header

tuned

force less agressively

lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed

removed complicated (and rarely helpful) error reporting

discontinued continuations to simplify control flow; dropped optimization in scnp

use Cache structure instead of passing tables around explicitly

merged

lemmas fold_commute and fold_commute_apply

spelling

adjusted to inductive characterization of sorted

tuned whitespace

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

turned distinct and sorted into inductive predicates: yields nice induction principles for free

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

some Poly/ML-specific debugging code escaped in the wild -- comment it out

merged

avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime

moved ML_Context.value to Code_Runtime

constant `contents` renamed to `the_elem`

merged

tune whitespace

rename bound variables after skolemizing, if the axiom of choice is available

tuning

rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)

tune bound names

merged

avoid dependency on "int"

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

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;