2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 wenzelm 2005-09-21 updated for Isabelle2005;
2005-09-21 wenzelm 2005-09-21 obsolete;
2005-09-21 paulson 2005-09-21 improved proof parsing
2005-09-21 paulson 2005-09-21 trying to limit the looping
2005-09-21 wenzelm 2005-09-21 updated for Isabelle2005;
2005-09-21 wenzelm 2005-09-21 new header syntax;
2005-09-21 haftmann 2005-09-21 introduces update_warn instead of overwrite_warn
2005-09-21 haftmann 2005-09-21 added AList.make, eq_fst, apr ...
2005-09-21 haftmann 2005-09-21 unify dist and main
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 wenzelm 2005-09-21 fixed cvs export;
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 wenzelm 2005-09-21 obsolete;
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 wenzelm 2005-09-21 the_default, the_list;
2005-09-21 wenzelm 2005-09-21 updated;
2005-09-21 wenzelm 2005-09-21 quote "value";
2005-09-21 wenzelm 2005-09-21 removed "--" argument; updated for Isabelle2005; tuned;
2005-09-21 wenzelm 2005-09-21 isatool fixheaders;
2005-09-21 berghofe 2005-09-21 Added new "value" command.
2005-09-21 berghofe 2005-09-21 Simplified code generator for numerals.
2005-09-21 berghofe 2005-09-21 Declared nat_number_of as code lemma.
2005-09-21 berghofe 2005-09-21 - Added eval_term function and value command - Fixed name clash problem in test_term
2005-09-21 wenzelm 2005-09-21 tunes;
2005-09-21 wenzelm 2005-09-21 updated for Isabelle2005;
2005-09-21 wenzelm 2005-09-21 HOL-Complex-Matrix: fixed deps;
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 wenzelm 2005-09-21 updated for Isabelle2005;
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-21 haftmann 2005-09-21 (name mess cleanup)
2005-09-21 haftmann 2005-09-21 introduced AList module
2005-09-21 haftmann 2005-09-21 removed assoc, overwrite
2005-09-21 haftmann 2005-09-21 added update_warn
2005-09-21 wenzelm 2005-09-21 tuned;
2005-09-20 wenzelm 2005-09-20 fixed proof script of lemma merges_same_conv (Why did it stop working?);
2005-09-20 wenzelm 2005-09-20 updated;
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 HOL/ex/Chinese.thy;
2005-09-20 wenzelm 2005-09-20 tuned;
2005-09-20 wenzelm 2005-09-20 more contributions;
2005-09-20 wenzelm 2005-09-20 tuned headers;
2005-09-20 wenzelm 2005-09-20 tuned header;
2005-09-20 wenzelm 2005-09-20 use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;
2005-09-20 wenzelm 2005-09-20 fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
2005-09-20 webertj 2005-09-20 bugfix in "zchaff_with_proofs"
2005-09-20 paulson 2005-09-20 fixed recursive-looking declaration
2005-09-20 paulson 2005-09-20 tidying, and support for axclass/classrel clauses
2005-09-20 paulson 2005-09-20 fixed syntax for sml/nj
2005-09-20 webertj 2005-09-20 undone the previous change: show_hyps not supported anymore
2005-09-20 webertj 2005-09-20 pointers to src/HOL/Tools/sat_solver.ML added in comments
2005-09-20 haftmann 2005-09-20 introduced AList module in favor of assoc etc.
2005-09-20 webertj 2005-09-20 new menu item show-sort-hypotheses to toggle show_hyps
2005-09-20 wenzelm 2005-09-20 HOL/ex/Chinese.thy; PROOFGENERAL_OPTIONS: no longer prefer xemacs;
2005-09-20 wenzelm 2005-09-20 HOL-ex: Library/Commutative_Ring.thy;
2005-09-20 wenzelm 2005-09-20 moved Tools/comm_ring.ML to Library;
2005-09-20 wenzelm 2005-09-20 added Commutative_Ring (from Main HOL);
2005-09-20 wenzelm 2005-09-20 Simplifier.inherit_bounds;
2005-09-20 wenzelm 2005-09-20 TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
2005-09-20 wenzelm 2005-09-20 get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;