src/HOL/Induct/Tree.ML
changeset 11046 b5f5942781a0
parent 11045 971a50fda146
child 11047 10c51288b00d
--- a/src/HOL/Induct/Tree.ML	Sat Feb 03 15:22:57 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      HOL/Induct/Tree.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer,  TU Muenchen
-    Copyright   1999  TU Muenchen
-
-Infinitely branching trees
-*)
-
-Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "tree_map_compose";
-
-val prems = Goal "(!!x. P x ==> Q (f x)) ==>  \
-   \    exists_tree P ts --> exists_tree Q (map_tree f ts)";
-by (induct_tac "ts" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-by (Fast_tac 1);
-qed "exists_map";
-