# HG changeset patch
# User berghofe
# Date 1004116013 -7200
# Node ID 9bd6e8e62a0661f5f7aa85c407723fe1d86dd32d
# Parent  38e20c036e375e7f81b90b1fb1d037c83489d7da
Eliminated occurrence of rule_format.

diff -r 38e20c036e37 -r 9bd6e8e62a06 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Oct 26 18:16:45 2001 +0200
+++ b/src/HOL/Lambda/Type.thy	Fri Oct 26 19:06:53 2001 +0200
@@ -93,7 +93,7 @@
   by force
 
 
-subsection {* @{text n}-ary function types *}
+subsection {* n-ary function types *}
 
 lemma list_app_typeD [rule_format]:
     "\<forall>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<longrightarrow> (\<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts)"
@@ -193,7 +193,7 @@
 qed
 
 lemma lift_typings [rule_format]:
-  "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> (e\<langle>i:U\<rangle>) \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
+  "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   apply (induct_tac ts)
    apply simp
   apply (intro strip)
@@ -214,7 +214,7 @@
   done
 
 lemma substs_lemma [rule_format]:
-  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. (e\<langle>i:T\<rangle>) \<tturnstile> ts : Ts \<longrightarrow>
+  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
      e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   apply (induct_tac ts)
    apply (intro strip)
@@ -370,7 +370,6 @@
           from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
             by cases auto
           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
-          from Var have SI: "?R a" by cases (simp_all add: Cons)
           from T have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t 0)
             (map (\<lambda>t. t[u/i]) as))[(u \<^sub>\<degree> a[u/i])/0] \<in> IT"
           proof (rule MI2)
@@ -385,8 +384,8 @@
                 show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''"
                   by (rule typing.Var) simp
               qed
-              from argT uIT uT show "a[u/i] \<in> IT"
-                by (rule SI[rule_format])
+              from Var have "?R a" by cases (simp_all add: Cons)
+              with argT uIT uT show "a[u/i] \<in> IT" by simp
               from argT uT show "e \<turnstile> a[u/i] : T''"
                 by (rule subst_lemma) simp
             qed