src/HOL/Library/FuncSet.thy
changeset 27183 0fc4c0f97a1b
parent 26106 be52145f482d
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu Jun 12 22:29:49 2008 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Jun 12 22:29:50 2008 +0200
     1.3 @@ -209,16 +209,4 @@
     1.4          g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
     1.5    by (blast intro: card_inj order_antisym)
     1.6  
     1.7 -
     1.8 -(*The following declarations generate polymorphic Skolem functions for 
     1.9 -  these theorems. Eventually they should become redundant, once this 
    1.10 -  is done automatically.*)
    1.11 -
    1.12 -declare FuncSet.Pi_I [skolem]
    1.13 -declare FuncSet.Pi_mono [skolem]
    1.14 -declare FuncSet.extensionalityI [skolem]
    1.15 -declare FuncSet.funcsetI [skolem]
    1.16 -declare FuncSet.restrictI [skolem]
    1.17 -declare FuncSet.restrict_in_funcset [skolem]
    1.18 -
    1.19  end