added map_cong to recdef
authornipkow
Thu, 17 Aug 2000 18:30:48 +0200
changeset 9639 51107e8149a0
parent 9638 1f62547edc0e
child 9640 8c6cf4f01644
added map_cong to recdef
src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Aug 17 16:23:50 2000 +0200
+++ b/src/HOL/List.ML	Thu Aug 17 18:30:48 2000 +0200
@@ -326,6 +326,8 @@
 by Auto_tac;
 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
+Prim.Add_recdef_congs [map_cong];
+
 Goal "(map f xs = []) = (xs = [])";
 by (case_tac "xs" 1);
 by Auto_tac;