equal
deleted
inserted
replaced
108 From lemma @{thm[source]ex_infinite_path} the existence of an infinite |
108 From lemma @{thm[source]ex_infinite_path} the existence of an infinite |
109 @{term A}-avoiding path starting in @{term s} follows, just as required for |
109 @{term A}-avoiding path starting in @{term s} follows, just as required for |
110 the contraposition. |
110 the contraposition. |
111 *} |
111 *} |
112 |
112 |
113 apply(erule contrapos2); |
113 apply(erule contrapos_pp); |
114 apply(simp add:wf_iff_no_infinite_down_chain); |
114 apply(simp add:wf_iff_no_infinite_down_chain); |
115 apply(erule exE); |
115 apply(erule exE); |
116 apply(rule ex_infinite_path); |
116 apply(rule ex_infinite_path); |
117 apply(auto simp add:Paths_def); |
117 apply(auto simp add:Paths_def); |
118 done |
118 done |