equal
deleted
inserted
replaced
1494 hence "(y, x) \<in> r" by (auto simp:children_def) |
1494 hence "(y, x) \<in> r" by (auto simp:children_def) |
1495 from 1[rule_format, OF this, folded h(2)] |
1495 from 1[rule_format, OF this, folded h(2)] |
1496 show "finite M" . |
1496 show "finite M" . |
1497 qed |
1497 qed |
1498 thus ?case |
1498 thus ?case |
1499 by (unfold subtree_children finite_Un, auto) |
1499 apply(subst subtree_children finite_Un) |
|
1500 apply(auto) |
|
1501 done |
1500 qed |
1502 qed |
1501 |
1503 |
1502 end |
1504 end |
1503 |
1505 |
1504 definition "pairself f = (\<lambda>(a, b). (f a, f b))" |
1506 definition "pairself f = (\<lambda>(a, b). (f a, f b))" |