src/HOL/Product_Type.thy
changeset 11425 4988fd27d6e6
parent 11032 83f723e86dac
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/Product_Type.thy	Fri Jul 13 18:28:46 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sun Jul 15 14:47:28 2001 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4  use "Product_Type_lemmas.ML"
     1.5  
     1.6  constdefs
     1.7 -  internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c"
     1.8 +  internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
     1.9    "internal_split == split"
    1.10  
    1.11  lemma internal_split_conv: "internal_split c (a, b) = c a b"