removed Add_recdef_congs [map_cong] (see Main.thy);
authorwenzelm
Tue Sep 05 18:47:27 2000 +0200 (2000-09-05)
changeset 98535c6425d83501
parent 9852 6ca7fcac3e23
child 9854 a1383b55ac05
removed Add_recdef_congs [map_cong] (see Main.thy);
src/HOL/List.ML
     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;