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