equal
deleted
inserted
replaced
103 apply clarify |
103 apply clarify |
104 apply (erule ssubst)+ |
104 apply (erule ssubst)+ |
105 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) |
105 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) |
106 apply (rename_tac x1) |
106 apply (rename_tac x1) |
107 apply (rule_tac t="%z. H(x1,z)" in subst_context) |
107 apply (rule_tac t="%z. H(x1,z)" in subst_context) |
108 apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g") |
108 apply (subgoal_tac "\<forall>y \<in> r-``{x1}. ALL z. <y,z>\<in>f <-> <y,z>\<in>g") |
109 apply (blast intro: transD) |
109 apply (blast intro: transD) |
110 apply (simp add: apply_iff) |
110 apply (simp add: apply_iff) |
111 apply (blast intro: transD sym) |
111 apply (blast intro: transD sym) |
112 done |
112 done |
113 |
113 |