src/HOL/Library/Cardinality.thy
changeset 51188 9b5bf1a9a710
parent 51143 0a2371e7ced3
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Library/Cardinality.thy	Tue Feb 19 17:01:06 2013 +0100
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Tue Feb 19 19:44:10 2013 +0100
     1.3 @@ -234,8 +234,6 @@
     1.4    dest!: finite_imageD intro: inj_onI)
     1.5  end
     1.6  
     1.7 -declare [[show_consts]]
     1.8 -
     1.9  instantiation integer :: card_UNIV begin
    1.10  definition "finite_UNIV = Phantom(integer) False"
    1.11  definition "card_UNIV = Phantom(integer) 0"