added map_cong to recdef
authornipkow
Thu Aug 17 18:30:48 2000 +0200 (2000-08-17)
changeset 963951107e8149a0
parent 9638 1f62547edc0e
child 9640 8c6cf4f01644
added map_cong to recdef
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Thu Aug 17 16:23:50 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Aug 17 18:30:48 2000 +0200
     1.3 @@ -326,6 +326,8 @@
     1.4  by Auto_tac;
     1.5  bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
     1.6  
     1.7 +Prim.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;