[isabelle] a line of type definition

Dear experts:
  I read line 2404 in Determinats.thy, which is listed as follows:

 definition trace :: "'a::semiring_1^'n^'n ⇒ 'a"
  where "trace A = setsum (λi. ((A$i)$i)) (UNIV::'n set)"

I can guess A is of type 'a matrix, returns a result with type 'a.    (informally)
This is the first time I meet the type cat operator ^, can some experts
interpret it?       
Or simply point me which tutorial material I should read .

Yongjian Li
Associate Research Professor, Ph.D
State Key Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences
Beijing, China

Tel: (+86)10 6266 1645
Email:lyj238 at ios.ac.cn
Homepage: http://lcs.ios.ac.cn/~lyj238

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.