NEWS
2016-09-20 eberlm 2016-09-20 NEWS: Normalized_Fraction.thy
2016-09-19 kuncar 2016-09-19 resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
2016-09-19 fleury 2016-09-19 # after multiset intersection and union symbol
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-19 wenzelm 2016-09-19 tuned;
2016-09-18 wenzelm 2016-09-18 clarified notation;
2016-09-16 traytel 2016-09-16 NEWS
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-09-14 wenzelm 2016-09-14 NEWS;
2016-09-14 wenzelm 2016-09-14 discontinued global etc/abbrevs;
2016-09-12 blanchet 2016-09-12 NEWS
2016-09-09 nipkow 2016-09-09 msetsum -> set_mset, msetprod -> prod_mset
2016-09-08 wenzelm 2016-09-08 option "checkpoint" helps to fine-tune global heap space management;
2016-09-07 wenzelm 2016-09-07 unfold_abs_def is enabled by default;
2016-09-05 wenzelm 2016-09-05 clarified obscure facts;
2016-09-05 fleury 2016-09-05 tuning multisets; more interpretations
2016-09-05 fleury 2016-09-05 add_mset constructor in multisets
2016-09-05 blanchet 2016-09-05 added warning
2016-09-01 wenzelm 2016-09-01 NEWS;
2016-08-14 blanchet 2016-08-14 updated NEWS
2016-08-12 wenzelm 2016-08-12 uniform ML and document antiquotations;
2016-08-11 wenzelm 2016-08-11 clarified antiquotations;
2016-08-11 nipkow 2016-08-11 tuned
2016-08-10 nipkow 2016-08-10 "split add" -> "split". Documented new modifier "split!"
2016-08-09 eberlm 2016-08-09 Tuned primes
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.
2016-08-06 wenzelm 2016-08-06 more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
2016-08-05 wenzelm 2016-08-05 Sidekick parser for isabelle-ml and sml mode;
2016-08-04 wenzelm 2016-08-04 NEWS;
2016-08-03 wenzelm 2016-08-03 include 'begin' and 'end' structure in text folds;
2016-08-02 wenzelm 2016-08-02 tuned;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-29 fleury 2016-07-29 more instantiations for multiset
2016-07-24 haftmann 2016-07-24 text antiquotation for locales (similar to classes)
2016-07-27 Manuel Eberl 2016-07-27 NEWS: Primes
2016-07-21 wenzelm 2016-07-21 merged
2016-07-20 wenzelm 2016-07-20 provide Pure.simp/simp_all, which only know about meta-equality;
2016-07-20 wenzelm 2016-07-20 completion templates for commands involving "begin ... end" blocks;
2016-07-20 wenzelm 2016-07-20 moved method "use" to Pure; more documentation;
2016-07-20 fleury 2016-07-20 more instantiations for multiset
2016-07-20 fleury 2016-07-20 adding mset_map to the simp rules
2016-07-16 wenzelm 2016-07-16 information about proof outline with cases (sendback);
2016-07-13 wenzelm 2016-07-13 semantic indentation for unstructured proof scripts;
2016-07-12 wenzelm 2016-07-12 merged
2016-07-12 wenzelm 2016-07-12 NEWS;
2016-07-12 fleury 2016-07-12 sharing simp rules between ordered monoids and rings
2016-07-12 wenzelm 2016-07-12 added action "isabelle.newline" (shortcut ENTER);
2016-07-11 wenzelm 2016-07-11 merged
2016-07-11 wenzelm 2016-07-11 NEWS;
2016-07-11 haftmann 2016-07-11 NEWS
2016-07-08 haftmann 2016-07-08 avoid to hide equality behind (output) abbreviation
2016-07-08 nipkow 2016-07-08 new style dummy_pats
2016-07-07 fleury 2016-07-07 more instantiations for multiset
2016-07-06 blanchet 2016-07-06 leverage new 'order' type class instantiation in multiset
2016-07-05 fleury 2016-07-05 instantiate multiset with multiset ordering
2016-07-04 wenzelm 2016-07-04 merged
2016-07-04 wenzelm 2016-07-04 NEWS;
2016-07-04 haftmann 2016-07-04 spelling
2016-07-04 haftmann 2016-07-04 combinator to build partial equivalence relations from a predicate and an equivalenc relation
2016-07-04 haftmann 2016-07-04 basic facts about almost everywhere fix bijections