2012-11-19 ago theorem status about oracles/futures is no longer printed by default;
2012-11-18 ago more generous tracing_limit, with explicit system option;
2012-11-18 ago adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
2012-11-17 ago NEWS;
2012-11-08 ago NEWS
2012-11-06 ago renamed Sledgehammer option
2012-10-22 ago incorporated constant chars into instantiation proof for enum;
2012-10-22 ago more detailed Prover IDE NEWS;
2012-10-21 ago merged
2012-10-19 ago Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-20 ago moved quite generic material from theory Enum to more appropriate places
2012-10-18 ago renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-16 ago support for more informative errors in lazy enumerations;
2012-10-12 ago more NEWS;
2012-10-12 ago simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
2012-10-11 ago simplified construction of fold combinator on multisets;
2012-10-10 ago efficient construction of red black trees from sorted associative lists
2012-10-08 ago consolidated names of theorems on composition;
2012-10-08 ago corrected NEWS
2012-10-04 ago some documentation of show_markup;
2012-09-28 ago smarter handling of tracing messages;
2012-09-22 ago some PIDE NEWS from this summer;
2012-09-21 ago renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-20 ago NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
2012-09-15 ago typeclass formalising bounded subtraction
2012-09-14 ago merged two commands
2012-09-12 ago renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-10 ago more explicit indication of legacy features;
2012-09-07 ago lattice instances for option type
2012-09-07 ago combinator Option.these
2012-09-04 ago NEWS; CONTRIBUTORS
2012-09-03 ago "isabelle logo" produces EPS and PDF format simultaneously;
2012-08-29 ago provide polyml-5.4.1 as regular component;
2012-08-29 ago renamed Position.str_of to;
2012-08-28 ago updated NEWS and CONTRIBUTORS
2012-08-27 ago clarified "isabelle logo";
2012-08-22 ago 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
2012-08-17 ago some explanations on isabelle components;
2012-08-14 ago support for 'typ' with explicit sort constraint;
2012-08-08 ago discontinued obsolete "isabelle makeall";
2012-08-07 ago discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
2012-08-06 ago "isabelle options" prints Isabelle system options;
2012-08-05 ago more on isabelle mkroot;
2012-08-03 ago simplified custom document/build script, instead of old-style document/IsaMakefile;
2012-07-31 ago document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
2012-07-28 ago discontinued obsolete Isabelle/build script;
2012-07-28 ago announce advanced support for Isabelle sessions and build management;
2012-07-28 ago discontinued special treatment of Proof General;
2012-07-23 ago restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-07-22 ago NEWS
2012-07-20 ago added MaSh to news
2012-07-19 ago export code relatively to master directory
2012-07-18 ago removed lie
2012-07-18 ago doc updates
2012-07-06 ago tuned;
2012-07-06 ago discontinued obsolete attribute "COMP";
2012-06-29 ago default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
2012-06-25 ago updated "isar-ref" manual, reduced remaining material in "ref" manual.
2012-06-21 ago NEWS and CONTRIBUTORS
2012-06-06 ago updated NEWS