src/HOL/Recdef.thy
changeset 11284 981ea92a86dd
parent 11165 3b69feb7d053
child 11454 7514e5e21cb8
     1.1 --- a/src/HOL/Recdef.thy	Thu May 03 18:22:36 2001 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Fri May 04 15:38:48 2001 +0200
     1.3 @@ -59,6 +59,7 @@
     1.4    inv_image_def
     1.5    measure_def
     1.6    lex_prod_def
     1.7 +  same_fst_def
     1.8    less_Suc_eq [THEN iffD2]
     1.9  
    1.10  lemmas [recdef_cong] = if_cong image_cong