src/HOL/List.thy
changeset 54863 82acc20ded73
parent 54600 ac54bc80a5cc
child 54868 bab6cade3cc5
     1.1 --- a/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -2065,13 +2065,13 @@
     1.4  
     1.5  lemma butlast_take:
     1.6    "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
     1.7 -by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
     1.8 +by (simp add: butlast_conv_take min.absorb1 min.absorb2)
     1.9  
    1.10  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
    1.11  by (simp add: butlast_conv_take drop_take add_ac)
    1.12  
    1.13  lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
    1.14 -by (simp add: butlast_conv_take min_max.inf_absorb1)
    1.15 +by (simp add: butlast_conv_take min.absorb1)
    1.16  
    1.17  lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
    1.18  by (simp add: butlast_conv_take drop_take add_ac)