src/HOL/Product_Type.thy
changeset 14190 609c072edf90
parent 14189 de58f4d939e1
child 14208 144f45277d5a
     1.1 --- a/src/HOL/Product_Type.thy	Mon Sep 15 12:27:13 2003 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Sep 15 14:00:43 2003 +0200
     1.3 @@ -276,10 +276,10 @@
     1.4  lemma curryI [intro!]: "f (a,b) ==> curry f a b"
     1.5    by (simp add: curry_def)
     1.6  
     1.7 -lemma curryD [dest]: "curry f a b ==> f (a,b)"
     1.8 +lemma curryD [dest!]: "curry f a b ==> f (a,b)"
     1.9    by (simp add: curry_def)
    1.10  
    1.11 -lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
    1.12 +lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
    1.13    by (simp add: curry_def)
    1.14  
    1.15  lemma curry_conv [simp]: "curry f a b = f (a,b)"