--- a/IOA/example/Lemmas.ML Thu Dec 01 17:35:03 1994 +0100
+++ b/IOA/example/Lemmas.ML Fri Dec 02 10:26:59 1994 +0100
@@ -232,14 +232,14 @@
(* 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";