src/HOL/Nominal/Examples/SN.thy
changeset 19972 89c5afe4139a
parent 19687 0a7c6d78ad6b
child 21107 e69c0e82955a
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Fri Jun 30 18:26:36 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sun Jul 02 17:27:10 2006 +0200
     1.3 @@ -217,7 +217,7 @@
     1.4    shows   "valid (pi\<bullet>\<Gamma>)"
     1.5  using a
     1.6  apply(induct)
     1.7 -apply(auto simp add: fresh_eqvt)
     1.8 +apply(auto simp add: fresh_bij)
     1.9  done
    1.10  
    1.11  (* typing judgements *)
    1.12 @@ -281,7 +281,7 @@
    1.13      using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
    1.14  next 
    1.15    case (t3 \<Gamma> \<sigma> \<tau> a t)
    1.16 -  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
    1.17 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
    1.18    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
    1.19  qed (auto)
    1.20