--- a/src/HOL/Lambda/Eta.thy Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Lambda/Eta.thy Sun Aug 12 18:53:03 2007 +0200
@@ -142,11 +142,13 @@
done
lemma rtrancl_eta_subst':
+ fixes s t :: dB
assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta
by induct (iprover intro: eta_subst)+
lemma rtrancl_eta_subst'':
+ fixes s t :: dB
assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
@@ -238,6 +240,7 @@
*}
theorem eta_case:
+ fixes s :: dB
assumes free: "\<not> free s 0"
and s: "s[dummy/0] => u"
shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u"