2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-10-01 blanchet 2010-10-01 merged
2010-10-01 blanchet 2010-10-01 tune whitespace
2010-10-01 blanchet 2010-10-01 rename bound variables after skolemizing, if the axiom of choice is available
2010-10-01 blanchet 2010-10-01 tuning
2010-10-01 blanchet 2010-10-01 rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
2010-10-01 blanchet 2010-10-01 tune bound names
2010-10-01 blanchet 2010-10-01 merged
2010-10-01 blanchet 2010-10-01 avoid dependency on "int"
2010-10-01 blanchet 2010-10-01 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
2010-10-01 blanchet 2010-10-01 added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
2010-10-01 blanchet 2010-10-01 compute quantifier dependency graph in new skolemizer
2010-10-01 blanchet 2010-10-01 tuning
2010-10-01 blanchet 2010-10-01 compute substitutions in new skolemizer
2010-09-30 blanchet 2010-09-30 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
2010-09-30 blanchet 2010-09-30 reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
2010-09-30 blanchet 2010-09-30 encode number of skolem assumptions in them, for more efficient retrieval later
2010-09-30 blanchet 2010-09-30 move functions closer to where they're used
2010-09-30 blanchet 2010-09-30 Skolemizer tweaking
2010-09-29 blanchet 2010-09-29 "meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
2010-09-29 blanchet 2010-09-29 finished renaming file and module
2010-09-29 blanchet 2010-09-29 rename file
2010-09-29 blanchet 2010-09-29 ignore Skolem assumption (if any)
2010-09-29 blanchet 2010-09-29 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
2010-09-29 blanchet 2010-09-29 first step towards a new skolemizer that doesn't require "Eps"
2010-10-22 wenzelm 2010-10-22 cumulative update of generated files (since bf164c153d10);
2010-10-22 wenzelm 2010-10-22 removed ML_old.thy, which is largely superseded by ML.thy;
2010-10-22 wenzelm 2010-10-22 more on "Canonical argument order"; tuned;
2010-10-22 wenzelm 2010-10-22 cover @{Isar.state};
2010-10-22 wenzelm 2010-10-22 more on "Style and orthography";
2010-10-22 wenzelm 2010-10-22 more on "Naming conventions"; tuned;
2010-10-22 wenzelm 2010-10-22 tuned;
2010-10-21 wenzelm 2010-10-21 more on "Style and orthography";
2010-10-21 wenzelm 2010-10-21 more refs;
2010-10-21 wenzelm 2010-10-21 preliminary material on "Concrete syntax and type-checking";
2010-10-20 wenzelm 2010-10-20 more on "Association lists", based on more succinct version of older material;
2010-10-20 wenzelm 2010-10-20 clarified "lists as a set-like container";
2010-10-19 wenzelm 2010-10-19 more robust treatment of "op IDENT";
2010-10-19 wenzelm 2010-10-19 more on messages;
2010-10-19 wenzelm 2010-10-19 more on synchronized variables;
2010-10-19 wenzelm 2010-10-19 tuned;
2010-10-19 wenzelm 2010-10-19 more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
2010-10-19 wenzelm 2010-10-19 misc tuning;
2010-10-18 wenzelm 2010-10-18 somewhat modernized version of "Thread-safe programming";
2010-10-18 wenzelm 2010-10-18 more robust examples: explicit @{assert} instead of unchecked output;
2010-10-18 wenzelm 2010-10-18 more on "Configuration options";
2010-10-18 wenzelm 2010-10-18 tuned;
2010-10-18 wenzelm 2010-10-18 more on "Basic data types"; tuned;
2010-10-17 wenzelm 2010-10-17 more on "Integers";
2010-10-17 wenzelm 2010-10-17 use continental paragraph style, which works better with mixture of (in)formal text; tuned skips and indents; tuned;
2010-10-17 wenzelm 2010-10-17 robustified "warn" environment if \parindent is zero (e.g. within itemize, description etc.);
2010-10-16 wenzelm 2010-10-16 more on "Basic ML data types";
2010-10-16 wenzelm 2010-10-16 more robust treatment of symbolic indentifiers (which may contain colons);
2010-10-16 wenzelm 2010-10-16 more examples;
2010-10-16 wenzelm 2010-10-16 tuned;
2010-10-16 wenzelm 2010-10-16 more on "Exceptions"; tuned;
2010-10-15 wenzelm 2010-10-15 more on "Exceptions";
2010-10-15 wenzelm 2010-10-15 more examples;
2010-10-15 wenzelm 2010-10-15 tuned chapter arrangement;
2010-10-15 wenzelm 2010-10-15 more examples; tuned;