2010-01-19 hoelzl 2010-01-19 Add transpose to the List-theory.
2010-01-04 wenzelm 2010-01-04 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 wenzelm 2010-01-04 discontinued old ISABELLE and ISATOOL environment settings;
2010-01-04 wenzelm 2010-01-04 discontinued special HOL_USEDIR_OPTIONS;
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum; corrected spelling
2009-12-11 wenzelm 2009-12-11 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;
2009-12-11 haftmann 2009-12-11 NEWS
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann 2009-12-04 merged, resolving minor conflicts
2009-12-04 haftmann 2009-12-04 NEWS
2009-12-04 wenzelm 2009-12-04 back to after-release mode;
2009-11-23 wenzelm 2009-11-23 more tuning for release;
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