NEWS
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
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