src/HOL/Product_Type.thy
changeset 14190 609c072edf90
parent 14189 de58f4d939e1
child 14208 144f45277d5a
equal deleted inserted replaced
14189:de58f4d939e1 14190:609c072edf90
   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