--- a/src/HOL/Induct/Tree.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Tree.thy Tue Nov 13 22:18:03 2001 +0100
@@ -19,9 +19,7 @@
"map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
- apply (induct t)
- apply simp_all
- done
+ by (induct t) simp_all
consts
exists_tree :: "('a => bool) => 'a tree => bool"
@@ -32,9 +30,6 @@
lemma exists_map:
"(!!x. P x ==> Q (f x)) ==>
exists_tree P ts ==> exists_tree Q (map_tree f ts)"
- apply (induct ts)
- apply simp_all
- apply blast
- done
+ by (induct ts) auto
end