NEWS
2013-08-30 blanchet 2013-08-30 renamed command to clarify connection with BNF
2013-08-30 blanchet 2013-08-30 updated news/contributors with BNF stuff
2013-08-29 wenzelm 2013-08-29 added action isabelle.complete, using standard jEdit keyboard shortcut;
2013-08-29 wenzelm 2013-08-29 some completion options;
2013-08-29 wenzelm 2013-08-29 GTK+ works better due to avoidance of default list view popups;
2013-08-28 wenzelm 2013-08-28 complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text; complete words >= 3 characters only; discontinued short word abbrev "Un" (see also fdd6e68e29d9 and e38e80686ce5);
2013-08-23 wenzelm 2013-08-23 clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL; just one src/Tools/ROOT;
2013-08-23 wenzelm 2013-08-23 obsolete (see 52790e3961fe);
2013-08-23 wenzelm 2013-08-23 added action isabelle.reset-font-size;
2013-08-23 wenzelm 2013-08-23 tuned -- some reformatting;
2013-08-20 krauss 2013-08-20 renamed theory Mrec to Legacy_Mrec, no longer included by default
2013-08-17 wenzelm 2013-08-17 NEWS;
2013-08-13 wenzelm 2013-08-13 discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub";
2013-08-13 wenzelm 2013-08-13 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-09 wenzelm 2013-08-09 NEWS;
2013-08-07 wenzelm 2013-08-07 more NEWS and CONTRIBUTORS;
2013-07-31 wenzelm 2013-07-31 NEWS;
2013-07-31 wenzelm 2013-07-31 simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-29 wenzelm 2013-07-29 NEWS; tuned description;
2013-07-27 wenzelm 2013-07-27 discontinued historic document formats;
2013-07-27 wenzelm 2013-07-27 avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
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