NEWS
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-18 blanchet 2012-04-18 Sledgehammer NEWS and CONTRIBUTORS
2012-04-18 haftmann 2012-04-18 dropped errorneous NEWS entry
2012-04-18 haftmann 2012-04-18 consolidated NEWS entries on fold
2012-04-18 haftmann 2012-04-18 grouped fold-related NEWS entries together
2012-04-18 haftmann 2012-04-18 grouped NEWS concerning relations together
2012-04-18 haftmann 2012-04-18 merged rename traces
2012-04-16 wenzelm 2012-04-16 repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);
2012-04-16 nipkow 2012-04-16 merged
2012-04-04 nipkow 2012-04-04 refined new tutorial announcement
2012-04-15 wenzelm 2012-04-15 some coverage of bundled declarations;
2012-04-15 wenzelm 2012-04-15 some coverage of unnamed contexts, which can be nested within other targets;
2012-04-14 wenzelm 2012-04-14 misc tuning for release;
2012-04-14 wenzelm 2012-04-14 revert changes of already published NEWS;
2012-04-14 wenzelm 2012-04-14 some updates for release;
2012-04-14 wenzelm 2012-04-14 more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
2012-04-13 Andreas Lochbihler 2012-04-13 Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2012-04-13 Andreas Lochbihler 2012-04-13 NEWS
2012-04-13 bulwahn 2012-04-13 NEWS
2012-04-11 wenzelm 2012-04-11 rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
2012-04-10 wenzelm 2012-04-10 some coverage of HOL/TPTP;
2012-04-06 haftmann 2012-04-06 abandoned almost redundant *_foldr lemmas
2012-04-06 haftmann 2012-04-06 no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-04-04 bulwahn 2012-04-04 documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
2012-04-02 nipkow 2012-04-02 new tutorial
2012-04-01 krauss 2012-04-01 less modest NEWS; CONTRIBUTORS
2012-04-01 krauss 2012-04-01 renamed import session back to Import, conforming to directory name; NEWS
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-30 haftmann 2012-03-30 power on predicate relations
2012-03-29 bulwahn 2012-03-29 announcing NEWS (cf. 446cfc760ccf)
2012-03-28 wenzelm 2012-03-28 clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME; clarified jEdit/README_BUILD;
2012-03-28 huffman 2012-03-28 merged
2012-03-27 huffman 2012-03-27 remove more redundant lemmas
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-27 huffman 2012-03-27 generalized lemma zpower_zmod
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-27 huffman 2012-03-27 generalize more div/mod lemmas
2012-03-27 huffman 2012-03-27 generalize some theorems about div/mod
2012-03-28 wenzelm 2012-03-28 updated to jedit-4.5.1;
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-24 wenzelm 2012-03-24 ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE); update for prospective jdk1.7.x component;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-22 haftmann 2012-03-22 more instructive 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