--- a/src/HOL/Lambda/ListApplication.thy Fri Oct 26 16:18:14 2001 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Fri Oct 26 16:49:10 2001 +0200
@@ -11,7 +11,7 @@
syntax
"_list_application" :: "dB => dB list => dB" (infixl "$$" 150)
syntax (symbols)
- "_list_application" :: "dB => dB => dB" (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
+ "_list_application" :: "dB => dB list => dB" (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
translations
"t $$ ts" == "foldl (op $) t ts"
--- a/src/HOL/Lambda/Type.thy Fri Oct 26 16:18:14 2001 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Oct 26 16:49:10 2001 +0200
@@ -182,8 +182,7 @@
apply auto
done
-lemma lifts_IT:
- "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
+lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
by (induct ts) auto
lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
@@ -362,7 +361,7 @@
with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'" by simp
then obtain Ts
where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts \<Rrightarrow> T'"
- and argsT: "(e\<langle>i:T\<rangle>) \<tturnstile> as : Ts"
+ and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
by (rule list_app_typeE)
from headT obtain T''
where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
@@ -418,7 +417,7 @@
by (rule typing.Var) simp
moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
by (rule substs_lemma)
- hence "(e\<langle>0:Ts \<Rrightarrow> T'\<rangle>) \<tturnstile> ?ls as : Ts"
+ hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
by (rule lift_typings)
ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
by (rule list_app_typeI)
@@ -433,7 +432,7 @@
next
case False
from Var have "rs \<in> lists {t. ?R t}" by simp
- moreover from nT obtain Ts where "(e\<langle>i:T\<rangle>) \<tturnstile> rs : Ts"
+ moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
by (rule list_app_typeE)
hence "rs \<in> lists ?ty" by (rule lists_typings)
ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"