On Mon, 28 Sep 2015, Roger H. wrote:
Hello,what is the difference between 'a and 'a' ? Can you give me an example?
Both are type variables, but of different name. The initial prime is always required for type variables. More primes belong to the regular identifier syntax of Isabelle, like x and x' for term variables.