# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306977110 -32400
# Node ID a72a04f3d6bf49b30a5662b9e80ed0f7df00ab3d
# Parent  db0ed02eba6ec3ab9f95712d0b2cdc4c91bd60c0# Parent  04f7c4ce8588a08a65e8159532c4cf05d42af20f
merge

diff -r 04f7c4ce8588 -r a72a04f3d6bf Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 01 22:55:14 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 02 10:11:50 2011 +0900
@@ -427,15 +427,17 @@
   apply (simp add: fresh_star_Un fresh_star_inter1)
   apply (simp add: alphas fresh_star_zero)
   apply auto[1]
+  apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: inter_eqvt)
+  apply blast
   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
-oops
-(*
-  apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)
+  apply (simp add: IntI image_eqI)
   apply (drule subsetD[OF supp_subst])
-  apply auto[1]
   apply (simp add: fresh_star_def fresh_def)
+  apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
+  apply (simp add: )
   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
-  apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt)
+  apply (metis inf1I inter_eqvt mem_def supp_eqvt )
   apply (rotate_tac 6)
   apply (drule sym)
   apply (simp add: subst_eqvt)
@@ -446,7 +448,7 @@
   apply (simp add: fresh_star_def fresh_def)
   apply blast
   done
-*)
+
 
 text {* Some Tests about Alpha-Equality *}