src/HOL/Product_Type.thy
changeset 25511 54db9b5080b8
parent 24844 98c006a30218
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Product_Type.thy	Fri Nov 30 20:13:03 2007 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 30 20:13:05 2007 +0100
     1.3 @@ -771,12 +771,11 @@
     1.4    Setup of internal @{text split_rule}.
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 -  internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
     1.9 +definition
    1.10 +  internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
    1.11 +where
    1.12    "internal_split == split"
    1.13  
    1.14 -lemmas [code func del] = internal_split_def
    1.15 -
    1.16  lemma internal_split_conv: "internal_split c (a, b) = c a b"
    1.17    by (simp only: internal_split_def split_conv)
    1.18