src/ZF/List.thy
changeset 13524 604d0f3622d6
parent 13509 6f168374652a
child 13611 2edf034c902a
     1.1 --- a/src/ZF/List.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/ZF/List.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -425,7 +425,7 @@
     1.4  
     1.5  (** New induction rules **)
     1.6  
     1.7 -lemma list_append_induct:
     1.8 +lemma list_append_induct [case_names Nil snoc, consumes 1]:
     1.9      "[| l: list(A);
    1.10          P(Nil);
    1.11          !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
    1.12 @@ -434,8 +434,6 @@
    1.13  apply (erule rev_type [THEN list.induct], simp_all)
    1.14  done
    1.15  
    1.16 -lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
    1.17 -
    1.18  lemma list_complete_induct_lemma [rule_format]:
    1.19   assumes ih: 
    1.20      "\<And>l. [| l \<in> list(A);