author | nipkow |
Thu, 16 Oct 1997 15:09:08 +0200 | |
changeset 3902 | 265a5d8ab88f |
parent 3901 | 8b09bc500f65 |
child 3903 | 1b29151a1009 |
src/HOL/List.ML | file | annotate | diff | comparison | revisions |
--- 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";