[isabelle] inductive + for



Dear list,

it appears that in a "for" clause for inductive definitions, I can only
list the parameters in their respective order. That is, I can't state
that the second parameter of a definition remains unchanged. Is this
intentional? It means that now I have to either reshuffle all uses of my
definition or prove a custom induction rule.

Cheers
Lars




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