prefer direct rotate_prems over old-style COMP;

tuned proofs -- prefer direct "rotated" instead of old-style COMP;

ignore morphism more explicitly; tuned headers;

some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing

adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions; noting further steps with FIXME

removed obsolete Admin material, which was for E 1.0-004 from 2009;

updated "isar-ref" manual, reduced remaining material in "ref" manual.

cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;

more on "Syntax translation functions";

more on "Applying translation rules";

discontinued slightly anochronistic examples;

more on syntax translations;

more on "Abstract syntax trees";

more explicit section "Syntax transformations";

avoid duplicate simp rules in norm_arith tactic

NEWS and CONTRIBUTORS

merged

Integrated set comprehension pointfree simproc.

Improved tactic for rewriting set comprehensions into pointfree form. Currently the simproc targets a term with an arbitrary number of conjuncts of form "x : S". The tactic should now handle all cases of this form.

Updated comment to reflect current state.

clarifying comment

sound monotonicity inference in the presence of "aggressive" helpers

less confusing error message

removed dead code

class target handles additional non-class term parameters appropriately

merged

add lemma to FinFun

fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users

tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings

pass more facts to LEO-II, in the light of latest evaluation

prevent an "Empty" exception (e.g. with Satallax, "mono_native")

tuning terminology