clarified

parameterize configurations by custom settings

Change coercion for RealDef to use function application (not composition)

revisiting Code_Prolog (cf. 6fe4abb9437b)

fixed postprocessing for term presentation in quickcheck; tuned spacing

enable Z3 in the test configuration

add "-?" to "nitrox" tool

clean up new Skolemizer code -- some old hacks are no longer necessary

specify proper defaults for Nitpick and Refute on TPTP + tuning

added "nitrox" tool (Nitpick for first-order TPTP problems) to components

made one more Metis example use the new Skolemizer

Metis examples use the new Skolemizer to test it

new version of Metis 2.3 (29 Dec. 2010)

remove newly added wrong logic

more precise failure reporting in Sledgehammer/SMT

avoid evil "export_without_context", which breaks if there are local "fixes"

more robust handling of variables in new Skolemizer

merged

added subsection on Scala specialities

added more judgement day provers

allowing special set comprehensions in values command; adding an example for special set comprehension in values

merged

adding documentation about the eval option in quickcheck

adapting Quickcheck_Prolog to latest changes

changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth

adapting mutabelle; exporting more Quickcheck functions

making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck

changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout

added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;

tuned;

dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

more direct loose_bvar1; tuned;

indentation;

update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);

added editor mode line;

isolate change of Proofterm.proofs in TPTP.thy from rest of session; qualified Proofterm.proofs to facilitate grepping;

list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin; exclude backup files;

updated contributed components

Z3 non-commercial usage may explicitly be declined

export status function to query whether Z3 has been activated for usage within Isabelle

merge

avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"

move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle

really be quiet

replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH

merged

standardized headers

generalized Caratheodory from algebra to ring_of_sets

add ring_of_sets and subset_class as basis for algebra

added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter

added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers

remove lie from documentation

let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now

make Minimizer honor "verbose" and "debug" options better

fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples

moved some configurations to AFP, and fixed others

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;

binder_tr: more informative exception;