src/HOL/Lambda/WeakNorm.thy

   apply (rule NF.App)
   apply simp
   done
 
 lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
-  listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
-  by (induct ts) simp+
+    listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
+    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
+  by (induct ts) simp_all
 
 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 (rule beta)
   apply (erule subst_Var_NF)
   done
 
 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)"
+    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_all
 
 lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
   apply (induct fixing: i set: NF)
   apply (frule listall_conj1)

   apply (erule typing.App)
   apply assumption
   done
 
 
-theorem type_NF: assumes T: "e \<turnstile>\<^sub>R t : T"
-  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
+theorem type_NF:
+  assumes "e \<turnstile>\<^sub>R t : T"
+  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
 proof induct
   case Var
   show ?case by (iprover intro: Var_NF)
 next
   case Abs