--- a/src/HOL/Lambda/Lambda.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy Fri Nov 25 19:09:44 2005 +0100
@@ -159,8 +159,8 @@
Normalization. \medskip *}
theorem subst_preserves_beta [simp]:
- "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
- by (induct set: beta) (simp_all add: subst_subst [symmetric])
+ "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
+ by (induct fixing: t i set: beta) (simp_all add: subst_subst [symmetric])
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
apply (induct set: rtrancl)
@@ -170,8 +170,8 @@
done
theorem lift_preserves_beta [simp]:
- "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>i. lift r i \<rightarrow>\<^sub>\<beta> lift s i)"
- by (induct set: beta) auto
+ "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
+ by (induct fixing: i set: beta) auto
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
apply (induct set: rtrancl)