default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);

removed generated stuff to avoid bit rot;

merged

Documented "incomplete" option of spark_end

Various improvements - show names of remaining VCs after spark_open and spark_vc - spark_status now also shows names of conclusions - spark_end now also accepts pending VCs, if "incomplete" option is given - VCs whose proofs contain oracles are no longer declared as proved in the corresponding *.prv file

no ml-platform-specific components

instantiate card_UNIV with nibble and code_numeral

change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code

add generic phantom type

added universal jdk-6u31 as standard component;

added ProofGeneral-4.1 as standard component, which allows to discontinue special choosefrom magic eventually;

merged

adding a useful remark in the reference

more tests on lxbroy[234], which are 4 core Xeon machines;

moved crontab to lxbroy2, one of the newer server machines; avoid macbroy27 for now due to spurious NFS issues;

some files for universal JDK 1.6.0_31 component;

corrected name of components file

prefer stderr for warnings

include jedut_build among canonical components

support for platform-specific components

correction: proper initialization of existing component

snippet to be sourced in user settings file in order to initialize components for a repository revision; the initialization is »liberal« since there is no obvious solution yet for components whose distribution is restricted

more standard filename for common components

updated crontab on macbroy27 and macbroy2;

use macbroy27 instead of macbroy28, which is broken for several weeks already;

reintroduced "t@" encoding, this time sound

compile

tuning

renamed experimental option

finished implementation of DFG type class output

more work on DFG type classes

more work on class support

generate type classes for polymorphic DFG format (SPASS)

avoid detour through terms

cleanly distinguish between type declarations and symbol declarations

removed old hack now that types and terms are cleanly distinguished in the data structure

added sorts to datastructure

robustness -- TFF1 does not support type classes

implement polymorphic DFG output, without type classes for now

added type arguments to "ATerm" constructor -- but don't use them yet

started adding polymophic SPASS output

tuning

removed support for unsorted DFG, now that SPASS 3.7 is no longer supported

merged, resolving conflict with 87c831e30f0a;

eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;

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

updated NEWS

updated docs

added "args_query" encodings

removed killed encodings from Metis examples

updated docs

killed most unsound encodings

generalized monotonic constructor optimisation so that it works with e.g. the product type

removed micro-optimization whose justification I can't recall

add missing timeout multiplier

avoid dumping definitions several times in LEO-II proofs

robust LEO-II setup that doesn't rely on ".leoatprc"

renamed TPTP commands to agree with Sutcliffe's terminology

don't use aggressive with HO ATP

more aggressive type argument optimization

use cover for "poly_guards" encoding

hack to make LEO-II perform better on TPTP THF problems

swap adjectives (cf. Google)

tweaked remote Vampire version

don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway