src/HOL/Hyperreal/HLim.thy
Thu, 12 Apr 2007 03:37:30 +0200 huffman moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
less more (0) tip