2007-11-21 wenzelm 2007-11-21 tuned;
2007-11-21 wenzelm 2007-11-21 include elapsed time for parallel sessions;
2007-11-21 wenzelm 2007-11-21 intern_skolem: disallow qualified names;
2007-11-21 haftmann 2007-11-21 fixed
2007-11-21 haftmann 2007-11-21 dropped diagnostic commands
2007-11-20 wenzelm 2007-11-20 tuned;
2007-11-20 wenzelm 2007-11-20 tuned spacing;
2007-11-20 wenzelm 2007-11-20 updated Proof General advertisement; tuned line breaks;
2007-11-20 wenzelm 2007-11-20 PolyML.SaveState.loadState: exit on failure;
2007-11-19 aspinall 2007-11-19 Init outer syntax after message setup to avoid spurious output.
2007-11-19 isatest 2007-11-19 update to most recent smlnj version
2007-11-19 wenzelm 2007-11-19 inform_file_processed: made even more robust against bad file specs;
2007-11-18 wenzelm 2007-11-18 removed unused inform_file_processed; proper_inform_file_processed: check before change (avoids non-linear update); avoid Path.explode here (liberal low-level file names);
2007-11-18 wenzelm 2007-11-18 init_empty: check before change (avoids non-linear update);
2007-11-15 aspinall 2007-11-15 Add thm_dep preference to menu, inadvertently missed off
2007-11-15 wenzelm 2007-11-15 tuned;
2007-11-15 wenzelm 2007-11-15 use -source instead of -target;
2007-11-15 wenzelm 2007-11-15 target 1.4 of JVM;
2007-11-15 wenzelm 2007-11-15 thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
2007-11-15 wenzelm 2007-11-15 isatool version: clarify that this is the *long* form;
2007-11-15 wenzelm 2007-11-15 ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
2007-11-15 wenzelm 2007-11-15 cover ISABELLE_IDENTIFIER;
2007-11-14 wenzelm 2007-11-14 README for E binary distribution;
2007-11-14 wenzelm 2007-11-14 tuned;
2007-11-13 paulson 2007-11-13 patching in the latest changes from Hurd
2007-11-13 wenzelm 2007-11-13 tuned;
2007-11-13 wenzelm 2007-11-13 some more items;
2007-11-13 nipkow 2007-11-13 updated
2007-11-13 berghofe 2007-11-13 Added JAR paper by Wenzel and Wiedijk.
2007-11-13 berghofe 2007-11-13 Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.
2007-11-13 berghofe 2007-11-13 Added TrueE to extraction_expand.
2007-11-13 berghofe 2007-11-13 Added new program extraction examples.
2007-11-13 berghofe 2007-11-13 New case studies for program extraction.
2007-11-13 berghofe 2007-11-13 Moved auxiliary lemmas to separate theory.
2007-11-13 berghofe 2007-11-13 Added new exampes Greatest_Common_Divisor and Euclid.
2007-11-13 berghofe 2007-11-13 Moved nat_eq_dec to Util.thy
2007-11-13 berghofe 2007-11-13 Moved nat_eq_dec and search to Util.thy
2007-11-13 berghofe 2007-11-13 Tuned.
2007-11-13 berghofe 2007-11-13 to_pred and to_set now save induction and case rule tags.
2007-11-12 wenzelm 2007-11-12 removed left-over text links from lynx conversion; removed umlauts (cannot assume iso-latin anymore, and not yet utf-8 either);
2007-11-12 wenzelm 2007-11-12 back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12 wenzelm 2007-11-12 changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-11-12 nipkow 2007-11-12 updates
2007-11-12 haftmann 2007-11-12 updated
2007-11-12 wenzelm 2007-11-12 reactivated default paragraph formatting for ``proof documents'';
2007-11-12 schirmer 2007-11-12 fixed typo;
2007-11-12 schirmer 2007-11-12 added signatures; tuned
2007-11-11 wenzelm 2007-11-11 abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; export standard_infer_types;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; dest;
2007-11-11 nipkow 2007-11-11 updates
2007-11-11 wenzelm 2007-11-11 avoid ML print in production code;
2007-11-11 wenzelm 2007-11-11 updated;
2007-11-11 wenzelm 2007-11-11 auto quickcheck: reduced messages;
2007-11-11 wenzelm 2007-11-11 notation works with any known constant (including fixes/abbrevs);
2007-11-11 wenzelm 2007-11-11 HOL-Statespace;
2007-11-11 wenzelm 2007-11-11 * HOL-Statespace;
2007-11-11 wenzelm 2007-11-11 restore interrupt handler on init;
2007-11-11 wenzelm 2007-11-11 abbrev: back to PrintMode.internal, which works at least half-way;