2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-08-13 haftmann 2015-08-13 qualified adjust_*
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2014-11-09 haftmann 2014-11-09 self-contained simp rules for dvd on numerals
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-17 wenzelm 2012-03-17 renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;