src/HOLCF/IOA/ABP/Lemmas.ML
changeset 5192 704dd3a6d47d
parent 4833 2e53109d4bc8
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:39:47 1998 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:44:27 1998 +0200
     1.3 @@ -45,13 +45,13 @@
     1.4  val list_ss = simpset_of List.thy;
     1.5  
     1.6  goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
     1.7 -by (List.list.induct_tac "l" 1);
     1.8 +by (induct_tac "l" 1);
     1.9  by (simp_tac list_ss 1);
    1.10  by (simp_tac list_ss 1);
    1.11  val hd_append =result();
    1.12  
    1.13  goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
    1.14 - by (List.list.induct_tac "l" 1);
    1.15 + by (induct_tac "l" 1);
    1.16   by (simp_tac list_ss 1);
    1.17   by (Fast_tac 1);
    1.18  qed"cons_not_nil";