src/HOL/NSA/CLim.thy
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