HOL/subset.thy, equalities.thy, mono.thy: new
HOL/Lfp.thy: now depends upon mono
HOL/Gfp.thy: depends upon Lfp, not just mono
(* Title: HOL/subset.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
subset = Fun