NEWS
2016-01-01 wenzelm 2016-01-01 more symbols;
2015-12-31 wenzelm 2015-12-31 misc tuning for release;
2015-12-31 wenzelm 2015-12-31 misc updates for release;
2015-12-31 wenzelm 2015-12-31 documentation for "isabelle jedit_client";
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-29 wenzelm 2015-12-29 more arrow symbols;
2015-12-29 wenzelm 2015-12-29 more arrow symbols;
2015-12-29 wenzelm 2015-12-29 support additional abbrevs;
2015-12-29 wenzelm 2015-12-29 isabelle console: print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <->;
2015-12-23 wenzelm 2015-12-23 NEWS;
2015-12-22 paulson 2015-12-22 Liouville theorem, Fundamental Theorem of Algebra, etc.
2015-12-21 wenzelm 2015-12-21 tuned spelling; tuned white-space;
2015-12-21 haftmann 2015-12-21 merged
2015-12-19 haftmann 2015-12-19 documentation on last state of the art concerning interpretation
2015-12-21 wenzelm 2015-12-21 more explicit ML profiling, with official Isabelle output;
2015-12-15 paulson 2015-12-15 New complex analysis material
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-07 haftmann 2015-12-07 clarified terminology
2015-12-07 paulson 2015-12-07 Merge
2015-12-07 wenzelm 2015-12-07 tuned;
2015-12-06 wenzelm 2015-12-06 tuned;
2015-12-01 Andreas Lochbihler 2015-12-01 add formalisation of Bourbaki-Witt fixpoint theorem
2015-11-25 wenzelm 2015-11-25 observe option "indent";
2015-11-22 wenzelm 2015-11-22 tuned;
2015-11-21 wenzelm 2015-11-21 tuned;
2015-11-18 ballarin 2015-11-18 Refine the supression of abbreviations for morphisms that are not identities.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-16 nipkow 2015-11-16 NEWS
2015-11-15 wenzelm 2015-11-15 merged
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-11-15 haftmann 2015-11-15 NEWS
2015-11-14 haftmann 2015-11-14 represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-13 wenzelm 2015-11-13 more documentation;
2015-11-12 wenzelm 2015-11-12 support short form for \<^theory_text>;
2015-11-11 Andreas Lochbihler 2015-11-11 cancel complementary terms as arguments to sup/inf in boolean algebras
2015-11-10 wenzelm 2015-11-10 added @{command}, @{method}, @{attribute};
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-11-09 wenzelm 2015-11-09 uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;
2015-11-09 wenzelm 2015-11-09 prefer explicit State panel;
2015-11-08 wenzelm 2015-11-08 added option timeout_scale;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07 wenzelm 2015-11-07 added @{undefined} with somewhat undefined symbol;
2015-11-06 wenzelm 2015-11-06 more formal treatment of control symbols;
2015-11-05 wenzelm 2015-11-05 symbolic syntax "\<comment> text";
2015-11-04 wenzelm 2015-11-04 document antiquotation @{footnote}; render \<^footnote> as pilcrow -- the rarely used \<paragraph> loses its interpretation;
2015-11-04 wenzelm 2015-11-04 NEWS;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-11-02 blanchet 2015-11-02 don't pollute local theory with needless names
2015-11-02 blanchet 2015-11-02 allow selectors and discriminators with same name as type