src/HOL/Real/float.ML
Wed, 13 Dec 2006 15:45:31 +0100 haftmann introduced mk/dest_numeral/number for mk/dest_binum etc.
Thu, 28 Sep 2006 23:42:32 +0200 wenzelm removed obsolete Real/document/root.tex;
less more (0) tip