NEWS
2012-03-17 wenzelm 2012-03-17 refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; actually make "raw_def" internal (cf. 80123a220219);
2012-03-17 wenzelm 2012-03-17 merged;
2012-03-17 haftmann 2012-03-17 generalized INF_INT_eq, SUP_UN_eq
2012-03-17 wenzelm 2012-03-17 'definition' no longer exports the foundational "raw_def";
2012-03-16 wenzelm 2012-03-16 merged
2012-03-16 paulson 2012-03-16 ZF news
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 wenzelm 2012-03-16 defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
2012-03-15 wenzelm 2012-03-15 Isabelle/jEdit supports user-defined Isar commands within the running session;
2012-03-15 wenzelm 2012-03-15 added ML antiquotation @{keyword};
2012-03-14 wenzelm 2012-03-14 Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
2012-03-13 wenzelm 2012-03-13 improved attribute "abs_def" to handle object-equality as well;
2012-03-12 noschinl 2012-03-12 NEWS
2012-03-07 haftmann 2012-03-07 less rigorous but more realistic migration recommendation; note on code generation of sets
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-02-28 blanchet 2012-02-28 spelling
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-22 bulwahn 2012-02-22 NEWS
2012-02-18 krauss 2012-02-18 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;