2011-01-12 wenzelm 2011-01-12 more FIXMEs concerning bad catch-all exception handlers;
2011-01-12 wenzelm 2011-01-12 eliminated obsolete print_sign_exn_unit;
2011-01-12 wenzelm 2011-01-12 reraise interrupts as usual;
2011-01-12 wenzelm 2011-01-12 avoid catch-all exception handler, presumably TERM was meant here;
2011-01-12 wenzelm 2011-01-12 disabled experimental treatment of replacement text for now, which leads to odd spacing and strange effects on non-poppler viewers;
2011-01-12 wenzelm 2011-01-12 observe line length limit;
2011-01-12 wenzelm 2011-01-12 smart_string_of_real: print integer values without fractional part;
2011-01-11 wenzelm 2011-01-11 tuned (cf. 2fe62d602681);
2011-01-11 wenzelm 2011-01-11 added dist/jedit symlink for convenience;
2011-01-11 wenzelm 2011-01-11 record versions of both jEdit and Isabelle;
2011-01-11 wenzelm 2011-01-11 updated to Isabelle2011;
2011-01-11 wenzelm 2011-01-11 isabelle version -i;
2011-01-11 haftmann 2011-01-11 NEWS
2011-01-11 bulwahn 2011-01-11 NEWS
2011-01-11 krauss 2011-01-11 eliminated duplication
2011-01-11 wenzelm 2011-01-11 merged
2011-01-11 haftmann 2011-01-11 tuned text
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2011-01-11 wenzelm 2011-01-11 clarified notion Position.is_reported; ML warning/error: retain non-reported clear-text position, notably when evaluating external ML files;
2011-01-10 wenzelm 2011-01-10 refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.; tuned offset_position_of;
2011-01-10 wenzelm 2011-01-10 refined ML_Lex.flatten: ensure proper separation of tokens;
2011-01-10 wenzelm 2011-01-10 ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);
2011-01-10 boehmes 2011-01-10 use just one data slot to VC-related information
2011-01-10 boehmes 2011-01-10 be more precise: also merge option values
2011-01-10 boehmes 2011-01-10 only print warning in a visible context (previously, the warning was printed more than once)
2011-01-10 boehmes 2011-01-10 dropped superfluous error message
2011-01-10 krauss 2011-01-10 removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
2011-01-10 wenzelm 2011-01-10 updated for polyml-5.4.0; discontinued old-fashioned POLY_HOME via path; more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;
2011-01-10 wenzelm 2011-01-10 made SML/NJ happy;
2011-01-10 wenzelm 2011-01-10 added merge_options convenience;
2011-01-10 wenzelm 2011-01-10 tuned string_of_int to avoid allocation for small integers;
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2011-01-10 wenzelm 2011-01-10 eliminated obsolete LargeInt -- Int is unbounded;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2011-01-10 bulwahn 2011-01-10 removing dead code; tuned
2011-01-10 bulwahn 2011-01-10 made SML/NJ happy
2011-01-09 wenzelm 2011-01-09 reverted 08240feb69c7 -- breaks positions of reports;
2011-01-09 wenzelm 2011-01-09 ML_trace: observe context visibility flag (import for Latex mode, for example);
2011-01-09 wenzelm 2011-01-09 more direct treatment of Position.end_offset; tuned;
2011-01-09 wenzelm 2011-01-09 discontinued unused end_line, end_column;
2011-01-09 wenzelm 2011-01-09 more scalable HTML.output_width;
2011-01-09 wenzelm 2011-01-09 refined comment (again);
2011-01-08 huffman 2011-01-08 merged
2011-01-08 huffman 2011-01-08 use proper syntactic types for 'syntax' commands
2011-01-08 huffman 2011-01-08 make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion
2011-01-08 huffman 2011-01-08 use full path for library imports
2011-01-08 huffman 2011-01-08 types -> type_synonym
2011-01-08 wenzelm 2011-01-08 updated NEOS_SERVER, which is now provided via settings;
2011-01-08 wenzelm 2011-01-08 renamed Sum_Of_Squares to Sum_of_Squares;
2011-01-08 wenzelm 2011-01-08 Ord_List.merge convenience;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2011-01-08 wenzelm 2011-01-08 added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);
2011-01-08 wenzelm 2011-01-08 tuned;
2011-01-08 wenzelm 2011-01-08 tuned;
2011-01-08 wenzelm 2011-01-08 tuned headers;
2011-01-07 wenzelm 2011-01-07 merged
2011-01-07 bulwahn 2011-01-07 adding example theory for list comprehension to set comprehension simproc
2011-01-07 bulwahn 2011-01-07 adopting proofs due to new list comprehension to set comprehension simproc
2011-01-07 bulwahn 2011-01-07 adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs