1.1 --- a/src/HOL/Library/FuncSet.thy	Fri Sep 27 13:24:29 2002 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Sep 27 16:44:50 2002 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     1.5    "compose A g f == \<lambda>x\<in>A. g (f x)"
     1.6  
     1.7 +print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
     1.8  
     1.9  
    1.10  subsection{*Basic Properties of @{term Pi}*}
    1.11 @@ -105,7 +106,6 @@
    1.12  lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
    1.13  by (simp add: Pi_def restrict_def)
    1.14  
    1.15 -
    1.16  lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
    1.17  by (simp add: Pi_def restrict_def)
    1.18