# HG changeset patch
# User huffman
# Date 1277919758 25200
# Node ID dbdbebec57dfcda66ae91524a9632dc11f415009
# Parent  5cbd5d5959f27fe401d2a08bce1a3e8a1414344a
change type of 'dimension' to 'a itself => nat

diff -r 5cbd5d5959f2 -r dbdbebec57df src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 10:26:02 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 10:42:38 2010 -0700
@@ -1582,21 +1582,13 @@
     independent (basis ` {..<d}) \<and>
     inj_on basis {..<d}"
 
-definition (in real_basis) dimension :: "'a set \<Rightarrow> nat" where
+definition (in real_basis) dimension :: "'a itself \<Rightarrow> nat" where
   "dimension x =
     (THE d. basis ` {d..} = {0} \<and> independent (basis ` {..<d}) \<and> inj_on basis {..<d})"
 
 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
 
-translations "DIM('t)" => "CONST dimension (CONST UNIV \<Colon> 't set)"
-
-typed_print_translation {*
-let
-  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
-    Syntax.const @{syntax_const "_type_dimension"} $ Syntax.term_of_typ show_sorts T;
-in [(@{const_syntax dimension}, card_univ_tr')]
-end
-*}
+translations "DIM('t)" == "CONST dimension (TYPE('t))"
 
 lemma (in real_basis) dimensionI:
   assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0}; independent (basis ` {..<d});
@@ -2067,7 +2059,7 @@
 
 (** move **)
 lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
-  apply(subst(2) span_basis[THEN sym]) unfolding basis_range by auto
+  apply(subst span_basis[THEN sym]) unfolding basis_range by auto
 
 lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
   apply(subst card_image) using basis_inj by auto