[isabelle-dev] pretty-printing of DIM('a)

[Makarius]

On 03/04/16 14:50, Lawrence Paulson wrote:
> The DIM('a) notation is introduced in Multivariate_Analysis/Euclidean_Space, for referring to the dimension of the Euclidean space designated by type ‘a. (See code snippet below.) Unfortunately, DIM(‘a) pretty-prints as card Basis, and the type reference is lost.

This was accidentally broken in 2012. See now:

changeset:   63128:7e5084ad95aa
user:        wenzelm
date:        Tue May 24 17:51:09 2016 +0200
files:       src/HOL/Multivariate_Analysis/Euclidean_Space.thy
description:
recovered printing of DIM('a) (cf. 899c9c4e4a4c);


	Makarius