src/HOL/Library/FuncSet.thy
changeset 17781 32bb237158a5
parent 15140 322485b816ac
child 19536 1a3a3cf8b4fa
     1.1 --- a/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:17 2005 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:18 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  translations
     1.6    "PI x:A. B" => "Pi A (%x. B)"
     1.7 -  "A -> B" => "Pi A (_K B)"
     1.8 +  "A -> B" => "Pi A (%_. B)"
     1.9    "%x:A. f" == "restrict (%x. f) A"
    1.10  
    1.11  constdefs