2012-11-06 blanchet 2012-11-06 renamed Sledgehammer option
2012-10-22 haftmann 2012-10-22 incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy
2012-10-22 wenzelm 2012-10-22 more detailed Prover IDE NEWS;
2012-10-21 webertj 2012-10-21 merged
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-18 blanchet 2012-10-18 renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-16 wenzelm 2012-10-16 support for more informative errors in lazy enumerations;
2012-10-12 wenzelm 2012-10-12 more NEWS;
2012-10-12 wenzelm 2012-10-12 simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
2012-10-11 haftmann 2012-10-11 simplified construction of fold combinator on multisets; more coherent name for fold combinator on multisets
2012-10-10 Andreas Lochbihler 2012-10-10 efficient construction of red black trees from sorted associative lists
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2012-10-08 haftmann 2012-10-08 corrected NEWS
2012-10-04 wenzelm 2012-10-04 some documentation of show_markup;
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-09-22 wenzelm 2012-09-22 some PIDE NEWS from this summer;
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-20 Andreas Lochbihler 2012-09-20 NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-09-14 blanchet 2012-09-14 merged two commands
2012-09-12 blanchet 2012-09-12 renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-10 wenzelm 2012-09-10 more explicit indication of legacy features;
2012-09-07 haftmann 2012-09-07 lattice instances for option type
2012-09-07 haftmann 2012-09-07 combinator Option.these
2012-09-04 Christian Sternagel 2012-09-04 NEWS; CONTRIBUTORS
2012-09-03 wenzelm 2012-09-03 "isabelle logo" produces EPS and PDF format simultaneously; more robust invocation of epstopdf: avoid filter mode;
2012-08-29 wenzelm 2012-08-29 provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-08-28 blanchet 2012-08-28 updated NEWS and CONTRIBUTORS
2012-08-27 wenzelm 2012-08-27 clarified "isabelle logo";
2012-08-22 wenzelm 2012-08-22 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
2012-08-17 wenzelm 2012-08-17 some explanations on isabelle components;
2012-08-14 wenzelm 2012-08-14 support for 'typ' with explicit sort constraint;
2012-08-08 wenzelm 2012-08-08 discontinued obsolete "isabelle makeall";
2012-08-07 wenzelm 2012-08-07 discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
2012-08-06 wenzelm 2012-08-06 "isabelle options" prints Isabelle system options;
2012-08-05 wenzelm 2012-08-05 more on isabelle mkroot;
2012-08-03 wenzelm 2012-08-03 simplified custom document/build script, instead of old-style document/IsaMakefile;
2012-07-31 wenzelm 2012-07-31 document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
2012-07-28 wenzelm 2012-07-28 discontinued obsolete Isabelle/build script;
2012-07-28 wenzelm 2012-07-28 announce advanced support for Isabelle sessions and build management;
2012-07-28 wenzelm 2012-07-28 discontinued special treatment of Proof General;
2012-07-23 haftmann 2012-07-23 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-07-22 haftmann 2012-07-22 NEWS
2012-07-20 blanchet 2012-07-20 added MaSh to news
2012-07-19 haftmann 2012-07-19 export code relatively to master directory
2012-07-18 blanchet 2012-07-18 removed lie
2012-07-18 blanchet 2012-07-18 doc updates
2012-07-06 wenzelm 2012-07-06 tuned;
2012-07-06 wenzelm 2012-07-06 discontinued obsolete attribute "COMP";
2012-06-29 wenzelm 2012-06-29 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 wenzelm 2012-06-25 updated "isar-ref" manual, reduced remaining material in "ref" manual.
2012-06-21 bulwahn 2012-06-21 NEWS and CONTRIBUTORS
2012-06-06 blanchet 2012-06-06 updated NEWS
2012-06-04 boehmes 2012-06-04 restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
2012-05-29 bulwahn 2012-05-29 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
2012-05-24 wenzelm 2012-05-24 discontinued support for Poly/ML 5.2.1;
2012-05-23 wenzelm 2012-05-23 discontinued obsolete method fastsimp / tactic fast_simp_tac;
2012-05-23 wenzelm 2012-05-23 merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;