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