2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2013-05-12 wenzelm 2013-05-12 decentralized historic settings;
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-01-15 wenzelm 2013-01-15 avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-03-17 wenzelm 2012-03-17 renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;