2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2011-01-14 wenzelm 2011-01-14 more precise import; eliminated global prems;
2011-01-14 wenzelm 2011-01-14 Thy_Load.begin_theory: maintain source specification of imports; Thy_Info.register_thy: reconstruct deps using original imports (important for ProofGeneral.inform_file_processed);
2011-01-14 hoelzl 2011-01-14 merged
2011-01-14 hoelzl 2011-01-14 integral on lebesgue measure is extension of integral on borel measure
2011-01-14 hoelzl 2011-01-14 tuned formalization of subalgebra
2011-01-14 hoelzl 2011-01-14 introduced integral syntax
2011-01-14 hoelzl 2011-01-14 tuned theorem order
2011-01-14 haftmann 2011-01-14 configuration file for mira
2011-01-13 wenzelm 2011-01-13 eliminated global prems; tuned proofs;
2011-01-13 wenzelm 2011-01-13 more precise pretty printing -- to accomodate Scala message layout;
2011-01-13 wenzelm 2011-01-13 less verbosity -- avoid slightly odd tracing information on warning channel;
2011-01-13 wenzelm 2011-01-13 updated Isabelle/jEdit limitations and workarounds;
2011-01-13 wenzelm 2011-01-13 full theory path enables loading parents via master directory and keeps files strictly separate;
2011-01-13 wenzelm 2011-01-13 Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
2011-01-13 wenzelm 2011-01-13 clarified split_thy_path;
2011-01-13 wenzelm 2011-01-13 less verbosity;
2011-01-12 huffman 2011-01-12 proper 'domain' class instance for 'a defl, with deflation combinator
2011-01-12 krauss 2011-01-12 documented Option.bind
2011-01-12 krauss 2011-01-12 CONTRIBUTORS
2011-01-12 wenzelm 2011-01-12 updated keywords;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2011-01-12 wenzelm 2011-01-12 updated to ProofGeneral-4.x;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2011-01-12 wenzelm 2011-01-12 tuned proof;
2011-01-12 wenzelm 2011-01-12 eliminated global prems; tuned proofs;
2011-01-12 wenzelm 2011-01-12 compile;
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;