NEWS
2017-08-22 Lars Hupel 2017-08-22 output syntax for pattern aliases
2017-08-21 Manuel Eberl 2017-08-21 HOL-Analysis: Convergent FPS and infinite sums
2017-08-21 wenzelm 2017-08-21 tuned;
2017-08-21 wenzelm 2017-08-21 tuned;
2017-08-21 wenzelm 2017-08-21 misc tuning and updates for release;
2017-08-20 wenzelm 2017-08-20 officially allow restart of Isabelle plugin;
2017-08-18 wenzelm 2017-08-18 merged
2017-08-18 wenzelm 2017-08-18 more NEWS;
2017-08-18 Lars Hupel 2017-08-18 syntax for pattern aliases
2017-08-17 eberlm 2017-08-17 NEWS: Removed constant subseq; subsumed by strict_mono
2017-08-17 wenzelm 2017-08-17 support for incremental update according to session graph structure;
2017-08-15 nipkow 2017-08-15 NEWS sorted_wrt
2017-08-15 wenzelm 2017-08-15 NEWS;
2017-08-06 haftmann 2017-08-06 do not fall back on nbe if plain evaluation fails
2017-08-02 haftmann 2017-08-02 simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping; sufficient to keep history stamps rather than complete historized data; semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized; clarified signature;
2017-07-28 blanchet 2017-07-28 introduced option for nat-as-int in SMT
2017-07-15 eberlm 2017-07-15 Updated NEWS
2017-07-03 wenzelm 2017-07-03 added command 'alias' and 'type_alias';
2017-06-30 wenzelm 2017-06-30 NEWS;
2017-06-23 wenzelm 2017-06-23 NEWS;
2017-06-20 haftmann 2017-06-20 deleting a code equation never leads to unimplemented function
2017-06-20 blanchet 2017-06-20 SMT news
2017-06-05 wenzelm 2017-06-05 HTML preview via builtin HTTP server;
2017-05-29 eberlm 2017-05-29 reorganised material on sublists
2017-05-15 wenzelm 2017-05-15 NEWS;
2017-05-05 Manuel Eberl 2017-05-05 NEWS: totient 1 = 1 now
2017-04-24 wenzelm 2017-04-24 tuned;
2017-04-24 wenzelm 2017-04-24 clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
2017-04-23 wenzelm 2017-04-23 tuned documentation;
2017-04-23 wenzelm 2017-04-23 clarified tool name -- more official status;
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-04-21 wenzelm 2017-04-21 merged
2017-04-21 wenzelm 2017-04-21 afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
2017-04-20 blanchet 2017-04-20 removed Old_SMT legacy module
2017-04-19 wenzelm 2017-04-19 optionally explore all sessions -- potentially slow, e.g. for AFP;
2017-04-19 wenzelm 2017-04-19 proper sections;
2017-04-18 wenzelm 2017-04-18 exclude theories from other sessions; clarified modules;
2017-04-18 wenzelm 2017-04-18 some documentation;
2017-04-12 haftmann 2017-04-12 more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function
2017-04-09 wenzelm 2017-04-09 NEWS;
2017-04-09 wenzelm 2017-04-09 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
2017-04-06 haftmann 2017-04-06 session containing computational algebra
2017-04-04 eberlm 2017-04-04 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
2017-03-19 wenzelm 2017-03-19 updated to jedit-5.4.0;
2017-03-10 haftmann 2017-03-10 restored surj as output abbreviation, amending 6af79184bef3
2017-03-02 ballarin 2017-03-02 Knaster-Tarski fixed point theorem and Galois Connections.
2017-03-01 wenzelm 2017-03-01 more uniform platform settings;
2017-02-28 wenzelm 2017-02-28 more detailed platform information;
2017-02-28 paulson 2017-02-28 Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
2017-02-27 paulson 2017-02-27 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
2017-02-27 wenzelm 2017-02-27 clarified defaults;
2017-02-26 wenzelm 2017-02-26 tuned whitespace;
2017-02-26 haftmann 2017-02-26 re-established AFP entry for FinFuns as library
2017-02-24 wenzelm 2017-02-24 avoid Unicode that conflicts with Isabelle symbol rendering;
2017-02-22 haftmann 2017-02-22 more precise NEWS and CONTRIBUTORS
2017-02-22 haftmann 2017-02-22 basic documentation for computations
2017-02-13 fleury 2017-02-13 renaming multiset simprocs
2017-02-04 wenzelm 2017-02-04 more uniform use of Reconstruct.clean_proof_of;
2017-01-17 wenzelm 2017-01-17 removed some old ASCII syntax;
2017-01-15 wenzelm 2017-01-15 clarified settings;