generate abs_induct rules for quotient types

tuned

corrected Nbe.static_value: ignore cached compilations; tuned

tuned heading

tuned name

improved threading of thy-values through interpret functions;

exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;

add option to transfer method for specifying variables not to generalize over

New tactic "word_bitwise" expands word equalities/inequalities into logic.

setup_lifting: no_code switch and supoport for quotient theorems

remove old TPTP CNF/FOF parser; always use Nik's new parser

more standard SZS output

Sledgehammer NEWS and CONTRIBUTORS

tuned SZS status output

update documentation (mostly based on feedback by Makarius)

added SZS status wrappers in TPTP mode

fixed Auto Nitpick's output

phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup

started integrating Nik's parser into TPTP command-line tools

merged

tuned

dropped errorneous NEWS entry

merged

consolidated NEWS entries on fold

grouped fold-related NEWS entries together

grouped NEWS concerning relations together

merged rename traces

fixed type interpretation; output now excludes parsed term; tuned;

more tptp testing support functions;

tuned text, improved dependencies

Lifting: generate more thms & note them & tuned

move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients

more friendly sendback rendering, using green and "frisches Steingrau";

more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);

approximative file position for Pure entities;

render last ML_TYPING only -- relevant for inline antiquotations like @{term};

flat presentation of collective markup;

add lemma Quotient_abs_induct

more usage of context blocks

use context block

lifting_setup generates transfer rule for rep of typedefs

use context block to organize typedef lifting theorems

avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files

compile

get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)

doc update

display more messages, now that more provers are run by default

added testing of tptp problem names;

tidied exception-handling relating to tptp problem names;

updated TPTP's ROOT.ML to include TPTP_Interpret;

retain ISABELLE_HOME_WINDOWS which is useful for jEdit to fold file names symbolically, but without DOS expansion that causes problems with Cygwin/Posix roundtrip (cf. 5a7903ba2dac);

updated to scala-2.9.2;

make transfer method more deterministic by using SOLVED' on some subgoals

accomodate ProofGeneral as Isabelle component, with adhoc version switch for Cygwin as before;

tuned the setup of lifting; generate transfer rules for typedef and Quotient thms

improved exception-handling in tptp; tuned;

simplified interpretation of '$i';

more cleaning of tptp tests;

improved tptp_graph robustness by relying on thy; reused cleanup code; improved messages;

improved tptp interpretation test thy

tuned comments

improved handling of quoted names in tptp import

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;