--- a/Tutorial/Lambda.thy	Sat Jan 22 16:37:00 2011 -0600
+++ b/Tutorial/Lambda.thy	Sat Jan 22 18:59:48 2011 -0600
@@ -105,18 +105,13 @@
   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)
 
-
-subsection {* Single-Step Beta-Reduction *}
-
-inductive 
-  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
-where
-  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
-| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
-| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
-| b4[intro]: "App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
-
-
+lemma fresh_fact:
+  assumes a: "atom z \<sharp> s"
+  and b: "z = y \<or> atom z \<sharp> t"
+  shows "atom z \<sharp> t[y ::= s]"
+using a b
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+   (auto simp add: lam.fresh fresh_at_base)
 
 
 end