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...

Larry


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

Is there any fundamental reason why a short-cut like

--- snip ---
inductive_relations
   wt_exp :: tyctx exp ty ("_ |-exp _ : _" [60,60] 60)
intros
 ...
monos
 ...
--- 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.