# HG changeset patch # User wenzelm # Date 995201248 -7200 # Node ID 4988fd27d6e6d9a6353bba024fdba0d24b7dfc78 # Parent aa0571fb96b9235d98f04f87080c6f5b71a9800e tuned; diff -r aa0571fb96b9 -r 4988fd27d6e6 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Jul 13 18:28:46 2001 +0200 +++ b/src/HOL/Product_Type.thy Sun Jul 15 14:47:28 2001 +0200 @@ -119,7 +119,7 @@ use "Product_Type_lemmas.ML" constdefs - internal_split :: "('a \ 'b => 'c) => 'a * 'b => 'c" + internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c" "internal_split == split" lemma internal_split_conv: "internal_split c (a, b) = c a b"