--- a/src/HOL/Library/FuncSet.thy Fri Sep 27 13:24:29 2002 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Sep 27 16:44:50 2002 +0200
@@ -39,6 +39,7 @@
compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
"compose A g f == \<lambda>x\<in>A. g (f x)"
+print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
subsection{*Basic Properties of @{term Pi}*}
@@ -105,7 +106,6 @@
lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
by (simp add: Pi_def restrict_def)
-
lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
by (simp add: Pi_def restrict_def)