src/HOL/Library/RBT_Impl.thy
changeset 66808 1907167b6038
parent 64246 15d1ee6e847b
child 67408 4a4c14b24800
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -1169,7 +1169,7 @@
     1.4            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
     1.5        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
     1.6            apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
     1.7 -by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
     1.8 +by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
     1.9  
    1.10  lemma rbtreeify_g_code [code]:
    1.11    "rbtreeify_g n kvs =
    1.12 @@ -1180,7 +1180,7 @@
    1.13            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
    1.14        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    1.15            apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
    1.16 -by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
    1.17 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
    1.18  
    1.19  lemma Suc_double_half: "Suc (2 * n) div 2 = n"
    1.20  by simp