src/HOL/Hyperreal/HDeriv.thy
Fri, 13 Apr 2007 00:07:52 +0200 huffman moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
less more (0) tip