NEWS
2013-07-27 wenzelm 2013-07-27 discontinued ISABELLE_DOC_FORMAT;
2013-07-13 wenzelm 2013-07-13 merged
2013-07-13 wenzelm 2013-07-13 NEWS;
2013-07-13 haftmann 2013-07-13 attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
2013-07-07 wenzelm 2013-07-07 discontinued obsolete "isabelle print";
2013-07-07 wenzelm 2013-07-07 discontinued command 'print_drafts';
2013-07-06 wenzelm 2013-07-06 minimal jedit mode for Isabelle NEWS;
2013-06-30 wenzelm 2013-06-30 discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-06-27 wenzelm 2013-06-27 updated documentation;
2013-06-25 wenzelm 2013-06-25 dockable window for Isabelle documentation;
2013-06-24 wenzelm 2013-06-24 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-23 wenzelm 2013-06-23 proper diagnostic command 'print_state';
2013-06-18 wenzelm 2013-06-18 eliminated old "ref" manual;
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2013-06-02 haftmann 2013-06-02 make reification part of HOL
2013-05-31 bulwahn 2013-05-31 NEWS about Spec_Check
2013-05-25 wenzelm 2013-05-25 merged
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
2013-05-22 wenzelm 2013-05-22 added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-17 wenzelm 2013-05-17 discontinued obsolete isabelle-process options -f and -u;
2013-05-17 wenzelm 2013-05-17 NEWS;
2013-05-17 wenzelm 2013-05-17 discontinued obsolete isabelle usedir, mkdir, make;
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25 hoelzl 2013-04-25 renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-04-23 haftmann 2013-04-23 documentation and NEWS
2013-04-22 hoelzl 2013-04-22 NEWS
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-10 wenzelm 2013-04-10 merged
2013-04-10 wenzelm 2013-04-10 added ML antiquotation @{theory_context};
2013-04-10 traytel 2013-04-10 NEWS and CONTRIBUTORS
2013-04-02 wenzelm 2013-04-02 NEWS for 635562bc14ef;
2013-03-27 ballarin 2013-03-27 Improvements to the print_dependencies command.
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-26 wenzelm 2013-03-26 dockable window for timing information;
2013-03-25 ballarin 2013-03-25 Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-23 haftmann 2013-03-23 spelling
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-23 haftmann 2013-03-23 locales for abstract orders
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