src/Pure/MLWorks.ML
Wed, 05 Mar 1997 10:02:53 +0100 paulson Now declares needs_filtered_use, but still unusable with current MLWorks
Fri, 06 Dec 1996 10:47:10 +0100 paulson MLWorks compatibility: it sort of works
less more (0) tip