--- a/Nominal/ExLet.thy Fri Mar 26 09:23:23 2010 +0100 +++ b/Nominal/ExLet.thy Fri Mar 26 10:07:26 2010 +0100 @@ -22,8 +22,6 @@ "bn Lnil = {}" | "bn (Lcons x t l) = {atom x} \<union> (bn l)" - - thm trm_lts.fv thm trm_lts.eq_iff thm trm_lts.bn