src/HOL/List.thy
changeset 55415 05f5fdb8d093
parent 55406 186076d100d3
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -1648,10 +1648,10 @@
     1.4  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
     1.5  apply (induct xs, simp, simp)
     1.6  apply safe
     1.7 -apply (metis nat_case_0 nth.simps zero_less_Suc)
     1.8 +apply (metis case_nat_0 nth.simps zero_less_Suc)
     1.9  apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
    1.10  apply (case_tac i, simp)
    1.11 -apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
    1.12 +apply (metis diff_Suc_Suc case_nat_Suc nth.simps zero_less_diff)
    1.13  done
    1.14  
    1.15  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"