Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Finite_Cartesian_Product.thy
changeset 30305 720226bedc4d
parent 30267 171b3bd93c90
parent 30304 d8e4cd2ac2a1
child 30488 5c4c3a9e9102 
--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Thu Mar 05 02:32:46 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Thu Mar 05 08:24:28 2009 +0100
@@ -15,7 +15,7 @@
 definition "dimindex (S:: 'a set) = (if finite (UNIV::'a set) then card (UNIV:: 'a set) else 1)"
 
 syntax "_type_dimindex" :: "type => nat" ("(1DIM/(1'(_')))")
-translations "DIM(t)" => "CONST dimindex (UNIV :: t set)"
+translations "DIM(t)" => "CONST dimindex (CONST UNIV :: t set)"
 
 lemma dimindex_nonzero: "dimindex S \<noteq>  0"
 unfolding dimindex_def
isabelle