src/ZF/Resid/Reduction.thy

 
 translations
   "Apl(n,m)" == "App(0,n,m)"
   
 inductive
-  domains       "lambda" <= "redexes"
+  domains       "lambda" <= redexes
   intros
     Lambda_Var:  "               n \<in> nat ==>     Var(n) \<in> lambda"
     Lambda_Fun:  "            u \<in> lambda ==>     Fun(u) \<in> lambda"
     Lambda_App:  "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda"
   type_intros    redexes.intros bool_typechecks

 (*     Lemmas for reduction                                                  *)
 (* ------------------------------------------------------------------------- *)
 
 lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
 apply (erule Sred.induct)
-apply (rule_tac [3] Sred.trans)
-apply simp_all
+apply (rule_tac [3] Sred.trans, simp_all)
 done
 
 lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
 apply (erule Sred.induct)
-apply (rule_tac [3] Sred.trans)
-apply simp_all
+apply (rule_tac [3] Sred.trans, simp_all)
 done
 
 lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
 apply (erule Sred.induct)
-apply (rule_tac [3] Sred.trans)
-apply simp_all
+apply (rule_tac [3] Sred.trans, simp_all)
 done
 
 lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
 apply (rule_tac n = "Apl (m',n) " in Sred.trans)
 apply (simp_all add: red_Apll red_Aplr)
 done
 
 lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>  
                Apl(Fun(m),n)---> n'/m'"
-apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans)
+apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans)
 apply (simp_all add: red_Apl red_Fun)
 done
 
 
 (* ------------------------------------------------------------------------- *)