NEWS
2012-02-17 wenzelm 2012-02-17 simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm 2012-02-16 simplified configuration options for syntax ambiguity;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-15 wenzelm 2012-02-15 discontinued obsolete "prems" fact;
2012-02-15 wenzelm 2012-02-15 NEWS;
2012-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2012-02-14 wenzelm 2012-02-14 tuned;
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-01-31 nipkow 2012-01-31 NEWS
2012-01-30 blanchet 2012-01-30 docs and news
2012-01-30 bulwahn 2012-01-30 NEWS
2012-01-19 blanchet 2012-01-19 renamed "sound" option to "strict"
2012-01-17 bulwahn 2012-01-17 refreshing NEWS
2012-01-16 wenzelm 2012-01-16 position constraints for numerals enable PIDE markup;
2012-01-10 bulwahn 2012-01-10 NEWS
2012-01-09 wenzelm 2012-01-09 misc tuning and reformatting;
2012-01-06 haftmann 2012-01-06 consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
2012-01-06 haftmann 2012-01-06 more explicit NEWS
2012-01-06 haftmann 2012-01-06 incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
2012-01-05 wenzelm 2012-01-05 discontinued Syntax.positions -- atomic parse trees are always annotated;
2012-01-05 wenzelm 2012-01-05 improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-12-28 huffman 2011-12-28 fix typos
2011-12-28 huffman 2011-12-28 remove some duplicate lemmas
2011-12-27 haftmann 2011-12-27 be explicit about Finite_Set.fold
2011-12-26 haftmann 2011-12-26 NEWS: unavoidable fact renames
2011-12-24 haftmann 2011-12-24 NEWS: `set` is now a proper type constructor
2011-12-23 huffman 2011-12-23 remove redundant lemma word_sub_def
2011-12-21 bulwahn 2011-12-21 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