# HG changeset patch
# User haftmann
# Date 1206011362 -3600
# Node ID cd956c4eadff9b166a5fcec4b4d9b25eb2a668ed
# Parent  6d437bde2f1d32cfe9e38ec83c7a452ce0550302
tuned proofs

diff -r 6d437bde2f1d -r cd956c4eadff src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Thu Mar 20 12:09:20 2008 +0100
+++ b/src/HOL/W0/W0.thy	Thu Mar 20 12:09:22 2008 +0100
@@ -204,11 +204,10 @@
        addsimps [thm "free_tv_subst"])) 1 *})
     apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
     apply simp
-   apply (tactic {* fast_tac (set_cs addss (@{simpset}
-     addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
-  -- {* @{text \<Longleftarrow>} *}
-  apply (unfold free_tv_subst cod_def dom_def)
+    apply (unfold free_tv_subst cod_def dom_def)
+    apply clarsimp
   apply safe
+  apply metis
   apply (metis linorder_not_less)+
   done
 
@@ -347,11 +346,8 @@
 lemma free_tv_comp_subst:
     "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   apply (unfold free_tv_subst dom_def)
-  apply (tactic {*
-    fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
-    thm "free_tv_subst_var" RS subsetD]
-    addss (@{simpset} delsimps (thms "bex_simps")
-    addsimps [thm "cod_def", thm "dom_def"])) 1 *})
+  apply (auto dest!: free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD]
+    simp add: cod_def dom_def simp del: bex_simps)
   done
 
 
@@ -746,8 +742,8 @@
    apply (frule_tac n = m in new_tv_W, assumption)
    apply (erule conjE)
    apply (drule free_tv_app_subst_tel [THEN subsetD])
-   apply (tactic {* fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_tv_list_le",
-     thm "codD", thm "new_tv_not_free_tv"]) 1 *})
+   apply (auto dest: W_var_geD [OF sym] new_tv_list_le
+     codD new_tv_not_free_tv)
   apply (case_tac "na \<in> free_tv t - free_tv sa")
    prefer 2
    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
@@ -758,7 +754,6 @@
    apply (drule free_tv_app_subst_tel [THEN subsetD])
    apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
      eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
-  apply fast
   done
 
 lemma W_complete: "[] |- e :: t' ==>