equal
deleted
inserted
replaced
274 by (simp add: curry_def split_def) |
274 by (simp add: curry_def split_def) |
275 |
275 |
276 lemma curryI [intro!]: "f (a,b) ==> curry f a b" |
276 lemma curryI [intro!]: "f (a,b) ==> curry f a b" |
277 by (simp add: curry_def) |
277 by (simp add: curry_def) |
278 |
278 |
279 lemma curryD [dest]: "curry f a b ==> f (a,b)" |
279 lemma curryD [dest!]: "curry f a b ==> f (a,b)" |
280 by (simp add: curry_def) |
280 by (simp add: curry_def) |
281 |
281 |
282 lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q" |
282 lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q" |
283 by (simp add: curry_def) |
283 by (simp add: curry_def) |
284 |
284 |
285 lemma curry_conv [simp]: "curry f a b = f (a,b)" |
285 lemma curry_conv [simp]: "curry f a b = f (a,b)" |
286 by (simp add: curry_def) |
286 by (simp add: curry_def) |
287 |
287 |