src/HOL/List.ML
changeset 9853 5c6425d83501
parent 9763 252c690690b0
child 10385 22836e4c5f4e
     1.1 --- a/src/HOL/List.ML	Tue Sep 05 18:47:03 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Sep 05 18:47:27 2000 +0200
     1.3 @@ -326,8 +326,6 @@
     1.4  by Auto_tac;
     1.5  bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
     1.6  
     1.7 -Add_recdef_congs [map_cong];
     1.8 -
     1.9  Goal "(map f xs = []) = (xs = [])";
    1.10  by (case_tac "xs" 1);
    1.11  by Auto_tac;