lemmas [recdef_cong] = map_cong;
authorwenzelm
Tue, 05 Sep 2000 18:47:46 +0200
changeset 9854 a1383b55ac05
parent 9853 5c6425d83501
child 9855 709a295731e2
lemmas [recdef_cong] = map_cong;
src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Sep 05 18:47:27 2000 +0200
+++ b/src/HOL/Main.thy	Tue Sep 05 18:47:46 2000 +0200
@@ -4,7 +4,8 @@
 
 theory Main = Map + String:
 
+(*actually belongs to theory List*)
 lemmas [mono] = lists_mono
+lemmas [recdef_cong] = map_cong 
 
 end
-