# HG changeset patch
# User wenzelm
# Date 1213302590 -7200
# Node ID 0fc4c0f97a1b4db7595b9566f0af49c81660df38
# Parent  9e4475b9d58c608cdb3c51eb240caedf7586ff20
removed obsolete skolem declarations -- done by Theory.at_end;

diff -r 9e4475b9d58c -r 0fc4c0f97a1b src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Thu Jun 12 22:29:49 2008 +0200
+++ b/src/HOL/Library/FuncSet.thy	Thu Jun 12 22:29:50 2008 +0200
@@ -209,16 +209,4 @@
         g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
   by (blast intro: card_inj order_antisym)
 
-
-(*The following declarations generate polymorphic Skolem functions for 
-  these theorems. Eventually they should become redundant, once this 
-  is done automatically.*)
-
-declare FuncSet.Pi_I [skolem]
-declare FuncSet.Pi_mono [skolem]
-declare FuncSet.extensionalityI [skolem]
-declare FuncSet.funcsetI [skolem]
-declare FuncSet.restrictI [skolem]
-declare FuncSet.restrict_in_funcset [skolem]
-
 end