src/HOL/Matrix_LP/Matrix.thy
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-09-24 wenzelm 2015-09-24 explicit indication of overloaded typedefs;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2013-12-25 haftmann 2013-12-25 abolished slightly odd global lattice interpretation for min/max
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
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;