Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed blunder in the setup of the classical reasoner wrt. the constant
authorskalberg
Mon, 15 Sep 2003 14:00:43 +0200
changeset 14190 609c072edf90
parent 14189 de58f4d939e1
child 14191 2014eac694d2
Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions 
--- 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