1.1 --- a/src/HOL/Induct/Tree.ML	Sat Feb 03 15:22:57 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,20 +0,0 @@
     1.4 -(*  Title:      HOL/Induct/Tree.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Stefan Berghofer,  TU Muenchen
     1.7 -    Copyright   1999  TU Muenchen
     1.8 -
     1.9 -Infinitely branching trees
    1.10 -*)
    1.11 -
    1.12 -Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
    1.13 -by (induct_tac "t" 1);
    1.14 -by (ALLGOALS Asm_simp_tac);
    1.15 -qed "tree_map_compose";
    1.16 -
    1.17 -val prems = Goal "(!!x. P x ==> Q (f x)) ==>  \
    1.18 -   \    exists_tree P ts --> exists_tree Q (map_tree f ts)";
    1.19 -by (induct_tac "ts" 1);
    1.20 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    1.21 -by (Fast_tac 1);
    1.22 -qed "exists_map";
    1.23 -