src/HOL/Data_Structures/Brother12_Set.thy
changeset 67613 ce654b0e6d69
parent 67406 23307fd33906
child 67929 30486b96274d
     1.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -456,7 +456,7 @@
     1.4    { case 2 with Suc.IH(1) show ?case by auto }
     1.5  qed auto
     1.6  
     1.7 -lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t : B (h+1) \<union> B h"
     1.8 +lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t \<in> B (h+1) \<union> B h"
     1.9  by(auto)
    1.10  
    1.11  lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"