IOA/example/Lemmas.ML

                 [succ_leq_mono, le_refl RS (leq_add_leq RS mp)]) 1);
 qed "plus_leq_lem";
 
 (* Lists *)
 
-goal List.thy "(L @ (x#M)) ~= []";
-  by (list_ind_tac "L" 1);
+goal List.thy "(xs @ (y#ys)) ~= []";
+  by (list.induct_tac "xs" 1);
   by (simp_tac list_ss 1);
   by (asm_simp_tac list_ss 1);
 qed "append_cons";
 
-goal List.thy "(X ~= hd(L@M)) = (X ~= if(L = [], hd(M), hd(L)))";
-  by (list_ind_tac "L" 1);
+goal List.thy "(x ~= hd(xs@ys)) = (x ~= if(xs = [], hd(ys), hd(xs)))";
+  by (list.induct_tac "xs" 1);
   by (simp_tac list_ss 1);
   by (asm_full_simp_tac list_ss 1);
 qed "not_hd_append";
 
 goal List.thy "(L = (x#rst)) --> (L = []) --> P";