src/HOL/Matrix_LP/ComputeFloat.thy
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2016-09-16 wenzelm 2016-09-16 more symbols;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-28 wenzelm 2015-12-28 more symbols;
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-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-22 wenzelm 2014-03-22 more antiquotations; clarified file location;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-13 wenzelm 2012-04-13 updated headers;
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;