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