Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Induct/Tree_Forest.thy
changeset 13535 007559e981c7
parent 12937 0c4fd7529467
child 16417 9bc16273c2d4 
--- a/src/ZF/Induct/Tree_Forest.thy	Tue Aug 27 11:09:33 2002 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy	Tue Aug 27 11:09:35 2002 +0200
@@ -45,7 +45,7 @@
   apply (rule Part_subset)
   done
 
-lemma treeI [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
+lemma treeI' [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)"
   by (rule forest_subset_TF [THEN subsetD])
 
 lemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)"
isabelle