[isabelle] shorter syntax?


I am proving things about lists of of values which have type of instances of comm_ring_1.
I have to write a lot of constructs like this:

fixes a::"'val::{comm_ring_1} list"

If there is a way to define shorter alias for this?
For example, before I was working with reals and I had
type_synonym 'vec' for 'real list' and I would use:

fixes a::"vec"

Any way to do something similar here?


Vadim Zaliva

CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

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