Removed map_compose from simpset.
authornipkow
Mon, 28 Aug 2000 17:02:19 +0200
changeset 9700 71364b487232
parent 9699 14dc0f812901
child 9701 533df6cedc2d
Removed map_compose from simpset.
src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Aug 28 16:53:35 2000 +0200
+++ b/src/HOL/List.ML	Mon Aug 28 17:02:19 2000 +0200
@@ -312,7 +312,7 @@
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "map_compose";
-Addsimps[map_compose];
+(*Addsimps[map_compose];*)
 
 Goal "rev(map f xs) = map f (rev xs)";
 by (induct_tac "xs" 1);