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