2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-14 hoelzl 2012-12-14 NEWS
2012-12-14 wenzelm 2012-12-14 merged
2012-12-13 Christian Sternagel 2012-12-13 renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS
2012-12-13 wenzelm 2012-12-13 smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-10 wenzelm 2012-12-10 more generous tracing limit -- rescaled in MB;
2012-12-06 wenzelm 2012-12-06 documentation for isabelle build_dialog and its implicit use in isabelle jedit;
2012-11-26 wenzelm 2012-11-26 tuned;
2012-11-26 wenzelm 2012-11-26 merged
2012-11-26 blanchet 2012-11-26 updated NEWS etc.
2012-11-26 wenzelm 2012-11-26 refined outer syntax 'help' command;
2012-11-25 wenzelm 2012-11-25 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
2012-11-24 wenzelm 2012-11-24 more NEWS/CONTRIBUTORS;
2012-11-24 wenzelm 2012-11-24 improved editing support for control styles; separate module for Isabelle actions;
2012-11-24 wenzelm 2012-11-24 added ISABELLE_PLATFORM_FAMILY;
2012-11-21 hoelzl 2012-11-21 NEWS: document changes in HOL-Probability
2012-11-21 hoelzl 2012-11-21 NEWS (changeset 13211e07d931): add Countable_Set
2012-11-21 hoelzl 2012-11-21 NEWS (changeset 69b35a75caf3): document changes in FuncSet
2012-11-21 nipkow 2012-11-21 new theory of immutable arrays
2012-11-20 wenzelm 2012-11-20 simplified command line of "isabelle install";
2012-11-19 wenzelm 2012-11-19 theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
2012-11-18 wenzelm 2012-11-18 more generous tracing_limit, with explicit system option;
2012-11-18 wenzelm 2012-11-18 adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
2012-11-17 wenzelm 2012-11-17 NEWS;
2012-11-08 bulwahn 2012-11-08 NEWS
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";