doc update

dropped dead code; tuned

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;