# HG changeset patch # User nipkow # Date 877007348 -7200 # Node ID 265a5d8ab88fb4cc57733c6d05064bbea8ae1176 # Parent 8b09bc500f655170e03471baafb753d857fa1e60 Removed comment. diff -r 8b09bc500f65 -r 265a5d8ab88f src/HOL/List.ML --- 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";