2009-04-02 wenzelm 2009-04-02 misc tuning for release;
2009-04-02 berghofe 2009-04-02 merged
2009-04-02 berghofe 2009-04-02 Fixed bug in transformation of congruence rule for == (thanks to Andy Schropp for reporting this).
2009-04-02 wenzelm 2009-04-02 some HOL-Nominal news;
2009-04-02 wenzelm 2009-04-02 updates for Isabelle2009 release;
2009-04-02 wenzelm 2009-04-02 tuned;
2009-04-02 wenzelm 2009-04-02 merged
2009-04-02 wenzelm 2009-04-02 misc cleanup and rearrangements for Isabelle2009 release;
2009-04-01 nipkow 2009-04-01 merged
2009-04-01 nipkow 2009-04-01 cleaned up setprod_zero-related lemmas
2009-04-01 huffman 2009-04-01 merged
2009-04-01 huffman 2009-04-01 generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
2009-04-01 nipkow 2009-04-01 added nat_div_gt_0 [simp]
2009-04-01 nipkow 2009-04-01 added setsum_pos_nat
2009-04-01 nipkow 2009-04-01 merged
2009-04-01 nipkow 2009-04-01 added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
2009-04-01 haftmann 2009-04-01 proper external tikz pictures
2009-04-01 wenzelm 2009-04-01 merged
2009-04-01 wenzelm 2009-04-01 tuned comments;
2009-04-01 wenzelm 2009-04-01 merged
2009-04-01 krauss 2009-04-01 explicitly check that at least one argument is present to avoid low-level exception
2009-04-01 wenzelm 2009-04-01 merged
2009-03-31 immler 2009-03-31 included managing_thread in state of AtpManager: synchronized termination and check for running managing_thread
2009-03-31 huffman 2009-03-31 domain package registers induction rules
2009-03-31 wenzelm 2009-03-31 merged
2009-03-31 ballarin 2009-03-31 Merged.
2009-03-31 ballarin 2009-03-31 Improvements to the text.
2009-03-31 wenzelm 2009-03-31 fixed header; misc simplification, use Conjunction.dest_conjunctions;
2009-03-31 wenzelm 2009-03-31 fixed header;
2009-03-31 wenzelm 2009-03-31 added dest_conjunctions (cf. Logic.dest_conjunctions);
2009-03-31 wenzelm 2009-03-31 superficial tuning;
2009-03-31 wenzelm 2009-03-31 merged
2009-03-31 wenzelm 2009-03-31 merged
2009-03-31 wenzelm 2009-03-31 schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
2009-03-31 wenzelm 2009-03-31 updated latex requirement;
2009-03-31 wenzelm 2009-03-31 tuned document;
2009-03-31 wenzelm 2009-03-31 replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp); modernized and tuned document;
2009-03-31 wenzelm 2009-03-31 tuned error message;
2009-03-31 wenzelm 2009-03-31 tuned;
2009-03-31 wenzelm 2009-03-31 suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;
2009-03-31 haftmann 2009-03-31 generalized pull to anamorph
2009-03-31 haftmann 2009-03-31 merged
2009-03-31 haftmann 2009-03-31 ML snippets for experimental evaluation
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 merged
2009-03-30 huffman 2009-03-30 domain package declares more simp rules
2009-03-30 wenzelm 2009-03-30 simplified 'print_orders' command;
2009-03-30 wenzelm 2009-03-30 tuned;
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 simplify theorem references
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-30 wenzelm 2009-03-30 tuned spacing and formatting;
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 immler 2009-03-30 terminate watching thread
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 no longer delay loading of assoc_fold.ML
2009-03-30 wenzelm 2009-03-30 qualified_name_of: observe empty case;
2009-03-30 wenzelm 2009-03-30 merged
2009-03-30 huffman 2009-03-30 merged