src/HOL/Library/RBT_Impl.thy
changeset 62390 842917225d56
parent 62093 bd73a2279fcd
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4  next
     1.5    case (Branch color t1 a b t2)
     1.6    let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
     1.7 -  have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
     1.8 +  have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: if_split_asm)
     1.9    moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp
    1.10    ultimately show ?case by (rule finite_subset)
    1.11  qed