using plain ISABELLE_PROCESS

merged

ignore ISABELLE_LINE_EDITOR for code generation

use long names for old-style fold combinators;

discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;

avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

end_timing: generalized result -- message plus with explicit time values;

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;

updated contributors;

removed parts of the manual that are clearly obsolete, or covered by newer manuals already (notably "isar-ref" or "implementation");

merged

minor update of Mercurial HOWTO;

removed redundant lemmas

added lemmas by Jeremy Avigad

A Serbian theory, by Filip Maric.

more accurate deps;

merged

add news for HOLCF; fixed some typos and inaccuracies

fixed headers;

moved isabelle_system.scala to src/Pure/System/;

moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);

updated generated files;

added method "coherent"; tuned formal markup;

more refs;

moved method "iprover" to HOL specific part;

removed Ids;

simultaneous use_thys;

replaced low-level 'no_syntax' by 'no_notation'; tuned header; tuned proofs;

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

tuned message;