src/ZF/List.thy

--- a/src/ZF/List.thy	Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/List.thy	Sun Jul 14 15:14:43 2002 +0200
@@ -439,6 +439,8 @@
 apply (erule rev_type [THEN list.induct], simp_all)
 done
 
+lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
+
 
 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)