NEWS
2011-12-14 bulwahn 2011-12-14 NEWS
2011-12-13 wenzelm 2011-12-13 'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-12-10 huffman 2011-12-10 prove class instances without extra lemmas
2011-12-09 huffman 2011-12-09 remove redundant lemma word_diff_minus
2011-12-09 noschinl 2011-12-09 more systematic lemma name
2011-12-05 bulwahn 2011-12-05 NEWS
2011-12-04 huffman 2011-12-04 remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
2011-12-01 blanchet 2011-12-01 added "minimize" option for more control over automatic minimization
2011-12-01 blanchet 2011-12-01 renamed "slicing" to "slice"
2011-12-01 wenzelm 2011-12-01 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-21 wenzelm 2011-11-21 NEWS;
2011-11-20 wenzelm 2011-11-20 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-11-19 wenzelm 2011-11-19 NEWS;
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes};
2011-11-17 huffman 2011-11-17 HOL-Word: removed more duplicate theorems
2011-11-17 huffman 2011-11-17 HOL-Word: removed many duplicate theorems (see NEWS)
2011-11-16 blanchet 2011-11-16 document "lam_trans" option
2011-11-09 wenzelm 2011-11-09 sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;
2011-11-07 blanchet 2011-11-07 avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
2011-11-07 wenzelm 2011-11-07 clarified attribute "mono_set": pure declaration, proper export in ML;
2011-11-07 wenzelm 2011-11-07 misc tuning;
2011-10-29 wenzelm 2011-10-29 uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
2011-10-28 wenzelm 2011-10-28 refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-10-21 bulwahn 2011-10-21 NEWS
2011-10-19 haftmann 2011-10-19 NEWS
2011-10-19 wenzelm 2011-10-19 inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19 bulwahn 2011-10-19 NEWS
2011-10-17 noschinl 2011-10-17 (old) NEWS
2011-10-14 haftmann 2011-10-14 NEWS
2011-10-13 wenzelm 2011-10-13 discontinued obsolete 'types' command;
2011-10-12 wenzelm 2011-10-12 discontinued obsolete alias structure ProofContext;
2011-10-09 huffman 2011-10-09 Int.thy: discontinued some legacy theorems
2011-09-26 wenzelm 2011-09-26 back to post-release mode;
2011-09-26 wenzelm 2011-09-26 tuned;
2011-09-26 wenzelm 2011-09-26 misc tuning for release;
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-22 huffman 2011-09-22 discontinued HOLCF legacy theorem names
2011-09-22 hoelzl 2011-09-22 NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-21 nipkow 2011-09-21 merged
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.
2011-09-20 haftmann 2011-09-20 official status for UN_singleton
2011-09-18 wenzelm 2011-09-18 tuned;
2011-09-18 wenzelm 2011-09-18 separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
2011-09-18 wenzelm 2011-09-18 some tuning and re-ordering for release;
2011-09-18 wenzelm 2011-09-18 misc tuning for release;
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-15 noschinl 2011-09-15 NEWS on Complete_Lattices, Lattices
2011-09-13 bulwahn 2011-09-13 correcting NEWS
2011-09-12 huffman 2011-09-12 NEWS and CONTRIBUTORS
2011-09-12 huffman 2011-09-12 remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12 huffman 2011-09-12 fix typos
2011-09-12 huffman 2011-09-12 NEWS for euclidean_space class
2011-09-12 hoelzl 2011-09-12 adding NEWS and CONTRIBUTORS
2011-09-12 bulwahn 2011-09-12 merged
2011-09-12 bulwahn 2011-09-12 adding NEWS and CONTRIBUTORS
2011-09-12 bulwahn 2011-09-12 tuned some symbol that probably went there by some strange encoding issue
2011-09-12 blanchet 2011-09-12 added my contributions to NEWS and CONTRIBUTORS
2011-09-12 nipkow 2011-09-12 NEWS fastsimp -> fastforce