src/HOL/Real/ContNotDenum.thy
Sun, 12 Feb 2006 12:29:01 +0100 kleing * include generalised MVT in HyperReal (contributed by Benjamin Porter)
less more (0) tip