src/HOL/List.ML
changeset 9700 71364b487232
parent 9639 51107e8149a0
child 9747 043098ba5098
     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);