src/HOL/ex/Gauge_Integration.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-06 wenzelm 2015-10-06 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-20 haftmann 2013-09-20 tuned proofs
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-02-16 bulwahn 2012-02-16 simplifying proof
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-02-24 huffman 2010-02-24 polished and converted some proofs to Isar style
2010-02-23 hoelzl 2010-02-23 Moved old Integration to examples.