Makarius wrote:
I would say it is virtually impossible to experiment with new commands
in Proof General. One needs to produce isabelle-keywords.el in batch
mode first, and then continue interactively.
My standard workaround is to edit isar-keywords.el manually, ignoring
the WARNING IN
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 = 'b_1) = ... = ('a_n = 'b_n)
= ('a_1, ..., 'a_n) k is = ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 = 'b_1) = ... = ('a_n = 'b_n)
= ('a_1, ..., 'a_n) k is = ('b_1, ..., 'b_n) k
for an n-ary
