--- a/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 10:30:06 2011 +0900
+++ b/Nominal/Ex/SFT/Lambda.thy	Fri Jun 24 10:54:31 2011 +0900
@@ -52,19 +52,19 @@
   by (relation "measure (\<lambda>(t,_,_). size t)")
      (simp_all add: lam.size)
 
-lemma subst4[eqvt]:
+lemma subst_eqvt[eqvt]:
   shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
   by (induct t x s rule: subst.induct) (simp_all)
 
-lemma subst1[simp]:
+lemma forget[simp]:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
   by (nominal_induct t avoiding: x s rule: lam.strong_induct)
      (auto simp add: lam.fresh fresh_at_base)
 
-lemma subst2[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
+lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
   by (simp add: fresh_def)
 
-lemma subst3[simp]: "M [x ::= V x] = M"
+lemma subst_id[simp]: "M [x ::= V x] = M"
   by (rule_tac lam="M" and c="x" in lam.strong_induct)
      (simp_all add: fresh_star_def lam.fresh fresh_Pair)