changeset 13356 | c9cfe1638bf2 |
parent 13339 | 0f89104dd377 |
child 13387 | b7464ca2ebbb |
--- 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. ***)