[isabelle-dev] NEWS: transitivity reasoner

2007-09-19 Thread Clemens Ballarin
* The transitivity reasoner for partial and linear orders is set up for locales `order' and `linorder' generated by the new class package. Previously the reasoner was only set up for axiomatic type classes. Instances of the reasoner are available in all contexts importing or interpreting

[isabelle-dev] NEWS

2007-09-19 Thread Makarius
* ML basics: just one true type int, which coincides with IntInf.int (even on SML/NJ).