tune type arg handling

tuning

fiddled with "tags_at" a bit -- the only non-tuning part of the change is a slight simplification of the typing axioms

remove needless type arguments to "tags_at" encoding

removed obsolete psbooklet;

more directory structure;

explicit is better than implicit;

removed obsolete rev_contrapos (cf. 1d195de59497);

tuned proofs -- eliminated old-fashioned COMP and rev_contrapos;

prefer sys.env from scala 2.9;

prefer sys.exit from scala 2.9;

internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;

more explicit directory structure Admin/Release/; updated to Admin/components;

merged

Stub theory for division on functionals.

slightly modernized ISABELLE_GHC etc. -- /usr/bin is more likely to provide it by default (notably on macbroy2[0-9] and lxbroy*);

more precise cover

don't generate any type class axioms for free types for monomorphic encodings

update docs

tuning

prefer hook in Admin/ to initialize components

corrected: avoid shadowing of variable

merged

adding some minimal documentation and an example of quickcheck's interfaces

exporting important function for the "many conjecture refutation" compilation of quickcheck

merged

new type class for computing finiteness of types with instantiations

add finiteness lemmas for 'a * 'b and 'a set

adding a challenging example in the examples file

eta-expanded occurences of algebraic functionals are simplified by default

not all Linuxen understand -Ssmpt= and defaults seem to be configured correctly now

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;