src/HOL/Library/FuncSet.thy
changeset 20770 2c583720436e
parent 20362 bbff23c3e2ca
child 21210 c17fd2df4e9e
     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:39 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Sep 28 23:42:43 2006 +0200
     1.3 @@ -39,8 +39,8 @@
     1.4    "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
     1.5  
     1.6  translations
     1.7 -  "PI x:A. B" == "Pi A (%x. B)"
     1.8 -  "%x:A. f" == "restrict (%x. f) A"
     1.9 +  "PI x:A. B" == "CONST Pi A (%x. B)"
    1.10 +  "%x:A. f" == "CONST restrict (%x. f) A"
    1.11  
    1.12  definition
    1.13    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"