Fun.thy
Fri, 19 Aug 1994 11:02:45 +0200 lcp HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
less more (0) tip