src/HOL/NSA/CLim.thy
Sun, 02 Nov 2014 17:13:28 +0100 wenzelm modernized header;
Sat, 01 Nov 2014 14:20:38 +0100 wenzelm eliminated spurious semicolons;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 07 May 2014 12:25:35 +0200 hoelzl avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Sun, 18 Aug 2013 19:59:19 +0200 wenzelm more symbols;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 29 May 2009 09:22:56 -0700 huffman generalize constants from Lim.thy to class metric_space
Thu, 03 Jul 2008 17:47:22 +0200 huffman move nonstandard analysis theories to NSA directory
less more (0) tip