2010-02-10 haftmann 2010-02-10 NEWS
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-06 wenzelm 2010-02-06 misc tuning;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22 haftmann 2010-01-22 NEWS
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;