NEWS
2009-11-23 haftmann 2009-11-23 tuned NEWS
2009-11-22 haftmann 2009-11-22 more uniform view on various number theory refinement steps
2009-11-22 wenzelm 2009-11-22 more NEWS, more tuning for release;
2009-11-22 wenzelm 2009-11-22 misc tuning and updates for official release;
2009-11-21 kleing 2009-11-21 wwwfind support currently for Linux only
2009-11-20 huffman 2009-11-20 NEWS: HOLCF changes since the last release
2009-11-20 kleing 2009-11-20 added NEWS item for wwwfind
2009-11-19 hoelzl 2009-11-19 Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
2009-11-13 nipkow 2009-11-13 -
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-11-12 bulwahn 2009-11-12 announcing the predicate compiler in NEWS and CONTRIBUTORS
2009-11-08 wenzelm 2009-11-08 updated functor Theory_Data, Proof_Data, Generic_Data;
2009-11-06 boehmes 2009-11-06 added documentation for local SMT solver setup and available SMT options, added verbose output for SMT solver invocation, test if local SMT solver exists before invoking it, always trace (possible) counterexamples, documented existence of SMT server
2009-11-06 krauss 2009-11-06 renamed method induct_scheme to induction_schema
2009-11-06 krauss 2009-11-06 NEWS
2009-11-03 boehmes 2009-11-03 added HOL-Boogie
2009-10-30 haftmann 2009-10-30 combined former theories Divides and IntDiv to one theory Divides
2009-10-28 paulson 2009-10-28 Probability tweaks
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-27 paulson 2009-10-27 merged
2009-10-27 paulson 2009-10-27 New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-26 blanchet 2009-10-26 merged
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.
2009-10-23 haftmann 2009-10-23 turned off old quickcheck
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 boehmes 2009-10-20 added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)
2009-10-18 nipkow 2009-10-18 certificates for sos
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 ballarin 2009-10-17 Merged.
2009-10-17 ballarin 2009-10-17 Finished revisions of locales tutorial.
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-09 haftmann 2009-10-09 term styles also cover antiquotations term_type and typeof
2009-10-08 haftmann 2009-10-08 new generalized concept for term styles
2009-10-01 ballarin 2009-10-01 News entry: inheritance of mixins; print_interps.
2009-09-30 haftmann 2009-09-30 merged
2009-09-30 haftmann 2009-09-30 mandatory prefix where appropriate
2009-09-29 wenzelm 2009-09-29 Synchronized and Unsynchronized;
2009-09-25 haftmann 2009-09-25 NEWS; corrected spelling
2009-09-22 haftmann 2009-09-22 merged
2009-09-21 haftmann 2009-09-21 added note on simp rules
2009-09-21 haftmann 2009-09-21 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-09-18 boehmes 2009-09-18 added new method "smt": an oracle-based connection to external SMT solvers
2009-09-18 haftmann 2009-09-18 INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-18 haftmann 2009-09-18 tuned NEWS, added CONTRIBUTORS
2009-09-17 paulson 2009-09-17 NEWS: New method metisFT
2009-09-16 haftmann 2009-09-16 Inter and Union are mere abbreviations for Inf and Sup; tuned
2009-09-01 haftmann 2009-09-01 corrected spelling
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-08-31 krauss 2009-08-31 moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-28 wenzelm 2009-08-28 discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28 wenzelm 2009-08-28 misc updates and tuning;
2009-08-21 boehmes 2009-08-21 added Mirabelle to NEWS
2009-08-12 wenzelm 2009-08-12 added PARALLEL_CHOICE, PARALLEL_GOALS;
2009-08-04 wenzelm 2009-08-04 etc/components; isabelle makeall operates on all components with IsaMakefile;
2009-07-29 nipkow 2009-07-29 sos documentation