--- a/src/HOL/Recdef.thy Thu May 03 18:22:36 2001 +0200
+++ b/src/HOL/Recdef.thy Fri May 04 15:38:48 2001 +0200
@@ -59,6 +59,7 @@
inv_image_def
measure_def
lex_prod_def
+ same_fst_def
less_Suc_eq [THEN iffD2]
lemmas [recdef_cong] = if_cong image_cong