changeset 26647 | 147c920ed5f7 |
parent 25107 | dbf09ca6a80e |
child 26677 | ab629324081c |
--- a/src/HOL/Nominal/Examples/Crary.thy Mon Apr 14 21:44:51 2008 +0200 +++ b/src/HOL/Nominal/Examples/Crary.thy Mon Apr 14 21:44:53 2008 +0200 @@ -458,7 +458,7 @@ apply(perm_simp) done -lemma test2: +lemma test2b: assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2" shows "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2" using a