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);