Re: [isabelle] short-cut for defining inductive relations

No fundamental reason that I can think of. Somebody simply has to find the energy to do this...


On 28 Mar 2006, at 13:31, Holger Gast wrote:

Is there any fundamental reason why a short-cut like

--- snip ---
   wt_exp :: tyctx exp ty ("_ |-exp _ : _" [60,60] 60)
--- snip ---

cannot replace the above four declarations by suitable
calls to the Isabelle interface functions?
Has anybody implemented it?

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