improved naming of 'distinct objects' in tptp import

reorganised tptp testing thys

enforced 'include' restrictions

tuned

split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL;

updated rel_comp ~> relcomp (cf. e1b761c216ac);

merged

more helpful error message

avoid option introduced in E 1.2 when invoking older versions of E

go back to the explicit compisition of quotient theorems

add theory data for relator identity rules; preprocess transfer rules generated by lift_definition using relator rules

note the Quotient theorem in quotient_type

leave Lifting prefix

more user aliases;

redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;

updated and clarified OF/MRS;

document attribute "abs_def";

repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);

merged

refined new tutorial announcement

merged

duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")

updated for release;

more precise handling of java failure, due to missing ISABELLE_JDK_HOME;

tuned some proofs; removed duplicate lemma zero_le_imp_of_nat

centralized enriched_type declaration, thanks to in-situ available Isar commands

tuned whitespace

replace locale 'UFT' with new un-named context block feature; use locale begin/end instead of 'in';

more CONTRIBUTORS;

some coverage of bundled declarations;

more uniform outline;

some coverage of unnamed contexts, which can be nested within other targets;

gathered mirabelle_sledgehammer's hardcoded defaults

Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action

Mirabelle now gives usage info when no arguments given

switched from using sed to perl in mirabelle tool

renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;

refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"; clarified thin_prems_tac: fail as tactic without error;

merged;

removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example

aligned tptp_graph dependencies to Isabelle conventions;

more ambitious isatest settings using polyml-svn (e.g. 1487);

use official TextArea.isCaretVisible and thus follow the "blink" flag; updated jedit_build component;

display more memory;

keyword ";" is declared via prover (as "minor", not "diag");

outermost SELECT_GOAL potentially improves performance;

report ISABELLE_HOME_WINDOWS;

chmod +x;

more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME;

misc tuning for release;

revert changes of already published NEWS;

some updates for release;

more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;

updated Scala/JVM versions;

include trailing comments in proper_command range;

minimal support for x86-mingw;

recognize MacOS on modern Java implementations, notably OpenJDK 1.7;

updated to Scala 2.9.2;

updated headers;

eliminated hard tabs;