src/HOL/W0/W0.thy
changeset 13601 fd3e3d6b37b2
parent 13537 f506eb568121
child 13890 90611b4e0054
     1.1 --- a/src/HOL/W0/W0.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/W0/W0.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -697,7 +697,7 @@
     1.4       apply (frule not_free_impl_id)
     1.5       apply simp
     1.6      txt {* @{text "na \<in> free_tv sa"} *}
     1.7 -    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
     1.8 +    apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
     1.9      apply (drule_tac eq_subst_tel_eq_free)
    1.10       apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
    1.11      apply simp
    1.12 @@ -733,7 +733,7 @@
    1.13      defer
    1.14      txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
    1.15      apply simp
    1.16 -    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
    1.17 +    apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
    1.18      apply (drule eq_subst_tel_eq_free)
    1.19       apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
    1.20      apply (simp add: free_tv_subst dom_def)
    1.21 @@ -881,7 +881,7 @@
    1.22     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
    1.23    apply (erule (1) notE impE)
    1.24    apply (erule exE conjE)+
    1.25 -  apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
    1.26 +  apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
    1.27    apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
    1.28     apply (simp add: new_tv_subst)
    1.29    apply (frule new_tv_subst_tel, assumption)