src/HOL/Recdef.thy
changeset 11284 981ea92a86dd
parent 11165 3b69feb7d053
child 11454 7514e5e21cb8
--- 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