equal
deleted
inserted
replaced
61 measure_def |
61 measure_def |
62 lex_prod_def |
62 lex_prod_def |
63 same_fst_def |
63 same_fst_def |
64 less_Suc_eq [THEN iffD2] |
64 less_Suc_eq [THEN iffD2] |
65 |
65 |
66 lemmas [recdef_cong] = if_cong image_cong |
66 lemmas [recdef_cong] = |
|
67 if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong |
67 |
68 |
68 lemma let_cong [recdef_cong]: |
69 lemma let_cong [recdef_cong]: |
69 "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" |
70 "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g" |
70 by (unfold Let_def) blast |
71 by (unfold Let_def) blast |
71 |
72 |