(* Title: HOL/Fun.thy ID: $Id$ Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Lemmas about functions. *) Fun = Set