src/HOL/Hyperreal/HLim.thy
Tue, 22 May 2007 21:32:04 +0200 huffman new simp rule Infinitesimal_of_hypreal_iff
Tue, 22 May 2007 19:47:55 +0200 huffman generalize uniqueness of limits to class real_normed_algebra_1
Fri, 18 May 2007 18:20:39 +0200 huffman minimize imports
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