equal
deleted
inserted
replaced
786 hide_const internal_split |
786 hide_const internal_split |
787 |
787 |
788 |
788 |
789 subsubsection {* Derived operations *} |
789 subsubsection {* Derived operations *} |
790 |
790 |
791 global consts |
791 definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where |
792 curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" |
792 "curry = (\<lambda>c x y. c (x, y))" |
793 |
|
794 local defs |
|
795 curry_def: "curry == (%c x y. c (Pair x y))" |
|
796 |
793 |
797 lemma curry_conv [simp, code]: "curry f a b = f (a, b)" |
794 lemma curry_conv [simp, code]: "curry f a b = f (a, b)" |
798 by (simp add: curry_def) |
795 by (simp add: curry_def) |
799 |
796 |
800 lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b" |
797 lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b" |