2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-06 haftmann 2010-05-06 constant name access lattice is not in use any longer
2010-05-06 wenzelm 2010-05-06 uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06 wenzelm 2010-05-06 replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06 wenzelm 2010-05-06 added separate;
2010-05-06 wenzelm 2010-05-06 basic formatting of pretty trees; line-up ML vs. Scala sources;
2010-05-06 wenzelm 2010-05-06 added content_length;
2010-05-06 wenzelm 2010-05-06 slightly more general Library.chunks;
2010-05-06 wenzelm 2010-05-06 misc tuning -- accumulate body via ListBuffer;
2010-05-06 wenzelm 2010-05-06 basic support for symbolic pretty printing; tuned;
2010-05-06 wenzelm 2010-05-06 extractors for document updates; Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;
2010-05-06 wenzelm 2010-05-06 extractors for outer keyword declarations;
2010-05-05 wenzelm 2010-05-05 eliminated deprecated "--" method; use case classes with copy method for functional record update;
2010-05-05 wenzelm 2010-05-05 use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
2010-05-05 wenzelm 2010-05-05 use SwingApplication instead of deprecated GUIApplication;
2010-05-05 wenzelm 2010-05-05 simplified via Position extractors;
2010-05-05 wenzelm 2010-05-05 some rearrangement of Scala sources;
2010-05-05 Cezary Kaliszyk 2010-05-05 fminus and some more theorems ported from Finite_Set.
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05 haftmann 2010-05-05 tuned whitespace
2010-05-05 haftmann 2010-05-05 tuned interpunctation, dropped dead comment
2010-05-04 huffman 2010-05-04 merged
2010-05-04 huffman 2010-05-04 avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)
2010-05-04 huffman 2010-05-04 generalize some lemmas to class t1_space
2010-05-04 huffman 2010-05-04 simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04 huffman 2010-05-04 generalize some lemmas
2010-05-04 huffman 2010-05-04 convert comments to 'text' blocks
2010-05-04 huffman 2010-05-04 generalize more lemmas about limits
2010-05-05 krauss 2010-05-05 repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-05-04 huffman 2010-05-04 merged
2010-05-04 huffman 2010-05-04 generalize types of LIMSEQ and LIM; generalize many lemmas
2010-05-04 huffman 2010-05-04 make (f -- a --> x) an abbreviation for (f ---> x) (at a)
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04 huffman 2010-05-04 adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-04 huffman 2010-05-04 declare cont_discrete_cpo [cont2cont]
2010-05-03 huffman 2010-05-03 remove unneeded constant Zseq
2010-05-03 huffman 2010-05-03 add lemmas eventually_nhds_metric and tendsto_mono
2010-05-03 huffman 2010-05-03 remove unneeded premise
2010-05-03 huffman 2010-05-03 add constants netmap and nhds
2010-05-04 ballarin 2010-05-04 Merged.
2010-05-04 ballarin 2010-05-04 Provide internal function for printing a single interpretation.
2010-04-27 ballarin 2010-04-27 Explicitly manage export in dependencies.
2010-05-04 wenzelm 2010-05-04 fixed proof (cf. edc381bf7200);
2010-05-04 hoelzl 2010-05-04 Corrected imports; better approximation of dependencies.
2010-05-04 hoelzl 2010-05-04 Add Convex to Library build
2010-05-04 hoelzl 2010-05-04 Removed unnecessary assumption
2010-05-04 Cezary Kaliszyk 2010-05-04 Translating lemmas from Finite_Set to FSet.
2010-05-04 wenzelm 2010-05-04 merged
2010-05-04 berghofe 2010-05-04 merged
2010-05-04 berghofe 2010-05-04 Turned Sem into an inductive definition.
2010-05-04 berghofe 2010-05-04 Corrected handling of "for" parameters.
2010-05-04 berghofe 2010-05-04 induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
2010-05-04 bulwahn 2010-05-04 added lemma about irreflexivity of pointer inequality in Imperative_HOL
2010-05-04 bulwahn 2010-05-04 added function ffilter and some lemmas from Finite_Set to the FSet theory
2010-05-04 haftmann 2010-05-04 merged
2010-05-04 haftmann 2010-05-04 avoid if on rhs of default simp rules
2010-05-04 krauss 2010-05-04 avoid exception Empty on malformed goal
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-05-04 haftmann 2010-05-04 a ring_div is a ring_1_no_zero_divisors
2010-05-04 haftmann 2010-05-04 NEWS