Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed Add_recdef_congs [map_cong] (see Main.thy);
authorwenzelm
Tue, 05 Sep 2000 18:47:27 +0200
changeset 9853 5c6425d83501
parent 9852 6ca7fcac3e23
child 9854 a1383b55ac05
removed Add_recdef_congs [map_cong] (see Main.thy);
src/HOL/List.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.ML	Tue Sep 05 18:47:03 2000 +0200
+++ b/src/HOL/List.ML	Tue Sep 05 18:47:27 2000 +0200
@@ -326,8 +326,6 @@
 by Auto_tac;
 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
-Add_recdef_congs [map_cong];
-
 Goal "(map f xs = []) = (xs = [])";
 by (case_tac "xs" 1);
 by Auto_tac;
isabelle