--- a/src/HOL/Lambda/WeakNorm.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Nov 25 19:09:44 2005 +0100
@@ -113,8 +113,8 @@
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
by (induct ts) simp+
-lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> (\<And>i j. t[Var i/j] \<in> NF)"
- apply (induct set: NF)
+lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
+ apply (induct fixing: i j set: NF)
apply simp
apply (frule listall_conj1)
apply (drule listall_conj2)
@@ -153,10 +153,10 @@
lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
- by (induct ts) simp+
+ by (induct ts) simp_all
-lemma lift_NF: "t \<in> NF \<Longrightarrow> (\<And>i. lift t i \<in> NF)"
- apply (induct set: NF)
+lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
+ apply (induct fixing: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)