changeset 17782 | b3846df9d643 |
parent 17456 | bcf7544875b2 |
child 20140 | 98acc6d0fab6 |
--- a/src/CCL/Type.thy Fri Oct 07 22:59:18 2005 +0200 +++ b/src/CCL/Type.thy Fri Oct 07 22:59:19 2005 +0200 @@ -41,9 +41,9 @@ translations "PROD x:A. B" => "Pi(A, %x. B)" - "A -> B" => "Pi(A, _K(B))" + "A -> B" => "Pi(A, %_. B)" "SUM x:A. B" => "Sigma(A, %x. B)" - "A * B" => "Sigma(A, _K(B))" + "A * B" => "Sigma(A, %_. B)" "{x: A. B}" == "Subtype(A, %x. B)" print_translation {*