NEWS
2013-03-13 wenzelm 2013-03-13 sessions may be organized via 'chapter' in ROOT;
2013-03-12 wenzelm 2013-03-12 discontinued "isabelle usedir" option -r (reset session path); simplified internal session identification: chapter / name; clarified chapter index (of sessions) vs. session index (of theories); discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser); removed obsolete session parent_path;
2013-03-11 wenzelm 2013-03-11 discontinued "isabelle usedir" option -P (remote path);
2013-03-09 haftmann 2013-03-09 discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
2013-02-28 wenzelm 2013-02-28 discontinued empty name bindings in 'axiomatization';
2013-02-28 wenzelm 2013-02-28 discontinued obsolete 'axioms' command;
2013-02-27 wenzelm 2013-02-27 discontinued redundant 'use' command;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2013-02-22 wenzelm 2013-02-22 discontinued obsolete src/HOL/IsaMakefile;
2013-02-16 haftmann 2013-02-16 restored proper order of NEWS entries (lost due too long-waiting patches)
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-15 blanchet 2013-02-15 updated news
2013-02-14 haftmann 2013-02-14 consolidation of library theories on product orders
2013-02-13 wenzelm 2013-02-13 merged;
2013-02-10 wenzelm 2013-02-10 updated PIDE notes;
2013-01-28 wenzelm 2013-01-28 tuned;
2013-01-26 wenzelm 2013-01-26 clarified NEWS on isabelle build and mkroot;
2013-01-25 wenzelm 2013-01-25 tuned;
2013-01-31 hoelzl 2013-01-31 remove unnecessary assumption from real_normed_vector
2013-01-20 wenzelm 2013-01-20 back to post-release mode -- after fork point;
2013-01-20 wenzelm 2013-01-20 updated for release;
2013-01-20 wenzelm 2013-01-20 misc tuning for release;
2013-01-14 kuncar 2013-01-14 NEWS
2013-01-11 wenzelm 2013-01-11 more NEWS;
2013-01-09 wenzelm 2013-01-09 tune spelling;
2013-01-08 wenzelm 2013-01-08 allow negative argument in "consumes" source format; more documentation/NEWS;
2013-01-04 wenzelm 2013-01-04 merged
2013-01-04 wenzelm 2013-01-04 more reactive completion popup by default;
2013-01-04 blanchet 2013-01-04 updated docs
2013-01-04 wenzelm 2013-01-04 more NEWS;
2013-01-04 wenzelm 2013-01-04 document 'locale_deps';
2013-01-03 wenzelm 2013-01-03 NEWS: ML runtime statistics;
2012-12-31 wenzelm 2012-12-31 misc tuning for release;
2012-12-31 wenzelm 2012-12-31 recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
2012-12-29 nipkow 2012-12-29 new theory Library/Finite_Lattice
2012-12-23 nipkow 2012-12-23 renamed and added lemmas
2012-12-18 haftmann 2012-12-18 discontinued legacy antiquotations and styles
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;