2010-06-14 haftmann 2010-06-14 corrected syntax diagram
2010-06-10 krauss 2010-06-10 Adapted Mirabelle script (cf. f60e4dd6d76f)
2010-06-14 wenzelm 2010-06-14 Added tag isa2009-2-test3 for changeset 0eacedd5f780
2010-06-14 wenzelm 2010-06-14 merged
2010-06-11 wenzelm 2010-06-11 NEWS: IsabelleText font;
2010-06-13 wenzelm 2010-06-13 Pretty.string_of (in Scala): actually observe margin/metric;
2010-06-13 wenzelm 2010-06-13 tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
2010-06-11 wenzelm 2010-06-11 tuned tooltips;
2010-06-09 wenzelm 2010-06-09 obsolete;
2010-06-09 wenzelm 2010-06-09 explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
2010-06-09 wenzelm 2010-06-09 contrib/README;
2010-06-09 wenzelm 2010-06-09 removed outdated/confusing INSTALL file;
2010-06-08 wenzelm 2010-06-08 clarified font_family vs. font_family_default; install_fonts: refrain from any magic that does not really work on Mac OS, but introduces strange problems on other platforms;
2010-06-08 wenzelm 2010-06-08 disable set_styles for now -- there are still some race conditions of PropertiesChanged vs. TextArea painting (NB: without it Isabelle_Token_Marker will crash if sub/superscript is actually used);
2010-06-07 wenzelm 2010-06-07 Added tag isa2009-2-test2 for changeset dfca6c4cd1e8
2010-06-07 wenzelm 2010-06-07 more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;
2010-06-07 wenzelm 2010-06-07 merged;
2010-06-07 berghofe 2010-06-07 Tuned.
2010-06-07 berghofe 2010-06-07 Documented changes in induct, cases, and nominal_induct method.
2010-06-07 wenzelm 2010-06-07 merged
2010-06-07 wenzelm 2010-06-07 made SML/NJ happy again;
2010-06-07 wenzelm 2010-06-07 recovered some untested theories;
2010-06-07 wenzelm 2010-06-07 proper target directory;
2010-06-07 wenzelm 2010-06-07 refer to isabelle-release branch;
2010-06-07 wenzelm 2010-06-07 no symlinks; tuned;
2010-06-07 wenzelm 2010-06-07 merged
2010-06-07 wenzelm 2010-06-07 tuned ANNOUNCEMENT;
2010-06-07 wenzelm 2010-06-07 more NEWS;
2010-06-07 wenzelm 2010-06-07 more NEWS; tuned;
2010-06-07 blanchet 2010-06-07 merged
2010-06-07 blanchet 2010-06-07 cosmetics
2010-06-05 blanchet 2010-06-05 renaming
2010-06-05 blanchet 2010-06-05 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 blanchet 2010-06-05 fix remote Vampire diagnosis
2010-06-05 blanchet 2010-06-05 make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; some of these aliases pop up only after Sledgehammer has converted the formula to CNF, so it can be very confusing to the user who said "add: foo del: bar" that "bar" is used in the end.
2010-06-05 blanchet 2010-06-05 totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax; faster and more reliable
2010-06-06 wenzelm 2010-06-06 single heaps archive;
2010-06-06 wenzelm 2010-06-06 merged
2010-06-06 wenzelm 2010-06-06 tuned;
2010-06-06 wenzelm 2010-06-06 removed obsolete dry-run option; just one archive for heaps, with the full cumulative collection (proper dependencies for rebuild);
2010-06-06 wenzelm 2010-06-06 Added tag isa2009-2-test1 for changeset d1cdbc7524b6
2010-06-05 haftmann 2010-06-05 merged
2010-06-04 haftmann 2010-06-04 avoid "$"
2010-06-04 haftmann 2010-06-04 tuned whitespace
2010-06-04 haftmann 2010-06-04 avoid flowerish abbreviation
2010-06-04 wenzelm 2010-06-04 merged
2010-06-04 blanchet 2010-06-04 merge
2010-06-04 blanchet 2010-06-04 don't raise Option.Option if assumptions contain schematic variables
2010-06-04 blanchet 2010-06-04 recongize one more outcome string for "remote_vampire"
2010-06-04 blanchet 2010-06-04 "print_vars_terms" wasn't doing its job properly; the offending line was "find_vars t1 #> find_vars t1", where the second "t1" should clearly have been "t2"
2010-06-04 blanchet 2010-06-04 merged
2010-06-04 blanchet 2010-06-04 made "clausify" attribute a legacy feature; seems to have ever only been a debugging feature
2010-06-04 blanchet 2010-06-04 made "neg_clausify" a legacy feature
2010-06-04 blanchet 2010-06-04 kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
2010-06-04 blanchet 2010-06-04 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
2010-06-04 blanchet 2010-06-04 fix bugs in Sledgehammer's Isar proof "redirection" code
2010-06-02 blanchet 2010-06-02 handle Vampire's definitions smoothly
2010-06-02 blanchet 2010-06-02 fix bug in direct Isar proofs, which was exhibited by the "BigO" example
2010-06-02 blanchet 2010-06-02 honor "xsymbols"
2010-06-02 blanchet 2010-06-02 kill another neg_clausify proof