Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Product_Type.thy
changeset 14190 609c072edf90
parent 14189 de58f4d939e1
child 14208 144f45277d5a 
--- a/src/HOL/Product_Type.thy	Mon Sep 15 12:27:13 2003 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 15 14:00:43 2003 +0200
@@ -276,10 +276,10 @@
 lemma curryI [intro!]: "f (a,b) ==> curry f a b"
   by (simp add: curry_def)
 
-lemma curryD [dest]: "curry f a b ==> f (a,b)"
+lemma curryD [dest!]: "curry f a b ==> f (a,b)"
   by (simp add: curry_def)
 
-lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
+lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
   by (simp add: curry_def)
 
 lemma curry_conv [simp]: "curry f a b = f (a,b)"
isabelle