src/HOL/Library/FinFun.thy
changeset 48051 53a0df441e20
parent 48041 d60f6b41bf2d
child 48059 f6ce99d3719b
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 16:05:21 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Thu May 31 16:58:38 2012 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Almost everywhere constant functions *}
     1.5  
     1.6  theory FinFun
     1.7 -imports Card_Univ
     1.8 +imports Cardinality
     1.9  begin
    1.10  
    1.11  text {*