Rationalized the rewriting of membership for {} and insert
by deleting the redundant theorems in_empty and in_insert
(* Title: HOL/subset.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge*)subset = Fun