# HG changeset patch
# User nipkow
# Date 786360419 -3600
# Node ID 61f39dcc1685f854e9f1adf61b29d48277b69273
# Parent  2adddba9892489ccd15d3dabe3af5de70bb27f63
list_ind_tac -> list.induct_tac

diff -r 2adddba98924 -r 61f39dcc1685 IOA/example/Lemmas.ML
--- 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";