--- a/src/HOL/Nominal/Examples/Weakening.thy Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy Sun Aug 12 18:53:03 2007 +0200
@@ -59,6 +59,7 @@
text {* Now it comes: The Weakening Lemma *}
lemma weakening_version1:
+ fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
and b: "valid \<Gamma>2"
and c: "\<Gamma>1 \<subseteq> \<Gamma>2"
@@ -97,7 +98,8 @@
with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto
qed (auto) (* app case *)
-lemma weakening_version3:
+lemma weakening_version3:
+ fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
and b: "valid \<Gamma>2"
and c: "\<Gamma>1 \<subseteq> \<Gamma>2"
@@ -120,6 +122,7 @@
is not strong enough - even this simple lemma fails to be simple ;o) *}
lemma weakening_too_weak:
+ fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
and b: "valid \<Gamma>2"
and c: "\<Gamma>1 \<subseteq> \<Gamma>2"