src/HOL/Lambda/NormalForm.thy

 (*  Title:      HOL/Lambda/NormalForm.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen, 2003
 *)
 
 header {* Inductive characterization of lambda terms in normal form *}
 

     case (App ts t)
     show ?case
     proof
       assume "Var t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> t'"
       then obtain rs where "ts => rs"
-	by (iprover dest: head_Var_reduction)
+        by (iprover dest: head_Var_reduction)
       with App show False
-	by (induct rs arbitrary: ts) auto
+        by (induct rs arbitrary: ts) auto
     qed
   next
     case (Abs t)
     show ?case
     proof

     case (2 u ts)
     show ?case
     proof (cases ts)
       case Nil
       from 2 have "\<forall>u'. \<not> u \<rightarrow>\<^sub>\<beta> u'"
-	by (auto intro: apps_preserves_beta)
+        by (auto intro: apps_preserves_beta)
       then have "NF u" by (rule 2)
       then have "NF (Abs u)" by (rule NF.Abs)
       with Nil show ?thesis by simp
     next
       case (Cons r rs)
       have "Abs u \<degree> r \<rightarrow>\<^sub>\<beta> u[r/0]" ..
       then have "Abs u \<degree> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
-	by (rule apps_preserves_beta)
+        by (rule apps_preserves_beta)
       with Cons have "Abs u \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
-	by simp
+        by simp
       with 2 show ?thesis by iprover
     qed
   qed
 qed