present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

added Future.cond_forks convenience;

Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;

tuned;

more direct loose_bvar1; tuned; slight re-unification of clone (cf. 47f8bfe0f597);

suppress Mercurial backup files; uniform treatment of tool filtering in bash/perl/scala;

updated generated file; tuned whitespace;

merged

SML_makeall: run with -j 3

fixed incomplete rename (1cdf54e845fa)

eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)

merged

changing iteration scheme of functions to use minimal number of function updates for exhaustive testing

added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)

mira interface to 'isabelle make' in addition to usedir and makeall; do not require dependencies

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