NEWS
2010-01-04 ago discontinued special HOL_USEDIR_OPTIONS;
2009-12-23 ago reduced code generator cache to the baremost minimum; corrected spelling
2009-12-11 ago Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
2009-12-11 ago NEWS
2009-12-05 ago tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 ago merged, resolving minor conflicts
2009-12-04 ago NEWS
2009-12-04 ago back to after-release mode;
2009-11-23 ago more tuning for release;
2009-11-23 ago tuned NEWS
2009-11-22 ago more uniform view on various number theory refinement steps
2009-11-22 ago more NEWS, more tuning for release;
2009-11-22 ago misc tuning and updates for official release;
2009-11-21 ago wwwfind support currently for Linux only
2009-11-20 ago NEWS: HOLCF changes since the last release
2009-11-20 ago added NEWS item for wwwfind
2009-11-19 ago Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
2009-11-13 ago -
2009-11-12 ago added a tabled implementation of the reflexive transitive closure
2009-11-12 ago New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-11-12 ago announcing the predicate compiler in NEWS and CONTRIBUTORS
2009-11-08 ago updated functor Theory_Data, Proof_Data, Generic_Data;
2009-11-06 ago added documentation for local SMT solver setup and available SMT options,
2009-11-06 ago renamed method induct_scheme to induction_schema
2009-11-06 ago NEWS
2009-11-03 ago added HOL-Boogie
2009-10-30 ago combined former theories Divides and IntDiv to one theory Divides
2009-10-28 ago Probability tweaks
2009-10-28 ago New theory Probability, which contains a development of measure theory
2009-10-27 ago merged
2009-10-27 ago New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-26 ago merged
2009-10-22 ago added Nitpick's theory and ML files to Isabelle/HOL;
2009-10-23 ago turned off old quickcheck
2009-10-22 ago inv_onto -> inv_into
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 ago added proof reconstructon for Z3,
2009-10-18 ago certificates for sos
2009-10-18 ago merged
2009-10-18 ago Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 ago Merged.
2009-10-17 ago Finished revisions of locales tutorial.
2009-10-17 ago operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-09 ago term styles also cover antiquotations term_type and typeof
2009-10-08 ago new generalized concept for term styles
2009-10-01 ago News entry: inheritance of mixins; print_interps.
2009-09-30 ago merged
2009-09-30 ago mandatory prefix where appropriate
2009-09-29 ago Synchronized and Unsynchronized;
2009-09-25 ago NEWS; corrected spelling
2009-09-22 ago merged
2009-09-21 ago added note on simp rules
2009-09-21 ago merged
2009-09-19 ago inter and union are mere abbreviations for inf and sup
2009-09-22 ago 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 ago added new method "smt": an oracle-based connection to external SMT solvers
2009-09-18 ago INTER and UNION are mere abbreviations for INFI and SUPR
2009-09-18 ago tuned NEWS, added CONTRIBUTORS
2009-09-17 ago NEWS: New method metisFT
2009-09-16 ago Inter and Union are mere abbreviations for Inf and Sup; tuned