| changeset 3902 | 265a5d8ab88f |
| parent 3896 | ee8ebb74ec00 |
| child 3919 | c036caebfc75 |
--- a/src/HOL/List.ML Thu Oct 16 14:52:35 1997 +0200 +++ b/src/HOL/List.ML Thu Oct 16 15:09:08 1997 +0200 @@ -530,10 +530,7 @@ by(Clarify_tac 1); by(Full_simp_tac 1); qed "in_set_butlast_appendI2"; -(* FIXME -Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2]; -AddIs [in_set_butlast_appendI1,in_set_butlast_appendI2]; -*) + (** take & drop **) section "take & drop";