src/HOL/Library/FuncSet.thy
changeset 20362 bbff23c3e2ca
parent 19736 d8d0f8f51d69
child 20770 2c583720436e
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:20 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Aug 08 18:40:56 2006 +0200
     1.3 @@ -219,4 +219,16 @@
     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