# HG changeset patch
# User wenzelm
# Date 1464105069 -7200
# Node ID 7e5084ad95aa6259ef44328ce1f97e222bd87a66
# Parent  0644c2e5a989c0584be85195cae044f71e59051d
recovered printing of DIM('a) (cf. 899c9c4e4a4c);

diff -r 0644c2e5a989 -r 7e5084ad95aa src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue May 24 16:24:20 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue May 24 17:51:09 2016 +0200
@@ -23,12 +23,13 @@
   assumes euclidean_all_zero_iff:
     "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
 
-abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where
-  "dimension TYPE('a) \<equiv> card (Basis :: 'a set)"
-
-syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
-
-translations "DIM('t)" == "CONST dimension (TYPE('t))"
+syntax "_type_dimension" :: "type \<Rightarrow> nat"  ("(1DIM/(1'(_')))")
+translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
+typed_print_translation \<open>
+  [(@{const_syntax card},
+    fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] =>
+      Syntax.const @{syntax_const "_type_dimension"} $ Syntax_Phases.term_of_typ ctxt T)]
+\<close>
 
 lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
   unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)