equal
deleted
inserted
replaced
1316 |
1316 |
1317 lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s" |
1317 lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s" |
1318 by (auto intro!: path_component_mem path_component_refl) |
1318 by (auto intro!: path_component_mem path_component_refl) |
1319 |
1319 |
1320 lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x" |
1320 lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x" |
1321 using assms |
|
1322 unfolding path_component_def |
1321 unfolding path_component_def |
1323 apply (erule exE) |
1322 apply (erule exE) |
1324 apply (rule_tac x="reversepath g" in exI) |
1323 apply (rule_tac x="reversepath g" in exI) |
1325 apply auto |
1324 apply auto |
1326 done |
1325 done |