changeset 11284 | 981ea92a86dd |
parent 11165 | 3b69feb7d053 |
child 11454 | 7514e5e21cb8 |
11283:358f82c4550d | 11284:981ea92a86dd |
---|---|
57 |
57 |
58 lemmas [recdef_simp] = |
58 lemmas [recdef_simp] = |
59 inv_image_def |
59 inv_image_def |
60 measure_def |
60 measure_def |
61 lex_prod_def |
61 lex_prod_def |
62 same_fst_def |
|
62 less_Suc_eq [THEN iffD2] |
63 less_Suc_eq [THEN iffD2] |
63 |
64 |
64 lemmas [recdef_cong] = if_cong image_cong |
65 lemmas [recdef_cong] = if_cong image_cong |
65 |
66 |
66 lemma let_cong [recdef_cong]: |
67 lemma let_cong [recdef_cong]: |