Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped spurious left-over from 0a2371e7ced3
authorhaftmann
Tue, 19 Feb 2013 19:44:10 +0100
changeset 51188 9b5bf1a9a710
parent 51187 c344cf148e8f
child 51189 a55ef201b19d
dropped spurious left-over from 0a2371e7ced3
src/HOL/Library/Cardinality.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Cardinality.thy	Tue Feb 19 17:01:06 2013 +0100
+++ b/src/HOL/Library/Cardinality.thy	Tue Feb 19 19:44:10 2013 +0100
@@ -234,8 +234,6 @@
   dest!: finite_imageD intro: inj_onI)
 end
 
-declare [[show_consts]]
-
 instantiation integer :: card_UNIV begin
 definition "finite_UNIV = Phantom(integer) False"
 definition "card_UNIV = Phantom(integer) 0"
isabelle