src/HOL/Lambda/StrongNorm.thy

 (*  Title:      HOL/Lambda/StrongNorm.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
     Copyright   2000 TU Muenchen
 *)
 
 header {* Strong normalization for simply-typed lambda calculus *}

         have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as"
           by (rule apps_preserves_beta) (rule beta.beta)
         with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
           by (rule subject_reduction)
         hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
-	  using uIT uT by (rule SI1)
+          using uIT uT by (rule SI1)
         thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
           by (simp del: subst_map add: subst_subst subst_map [symmetric])
         from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
           by (rule list_app_typeE) fast
         then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all