# HG changeset patch
# User nipkow
# Date 966529848 -7200
# Node ID 51107e8149a00f0ce8c17faac5a5bc8f6504c616
# Parent  1f62547edc0e14755cc47722092196e7b4af639f
added map_cong to recdef

diff -r 1f62547edc0e -r 51107e8149a0 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;