Re: [isabelle] adm and fixrec’s induct rules

Hi Brian,

Am Mittwoch, den 08.09.2010, 06:39 -0700 schrieb Brian Huffman:
> Sorry, I guess what I said was a bit misleading. There is no "foo_rec"
> constant. I only meant "foo_rec" to stand for the functional (a
> possibly large lambda term) of which "foo" is the least fixed-point.

ah, I see. Although it would be nice to have the foo_chain defined, in
my case, it would be too ugly (the lambda-term I’d have to copy’n’paste
would just be too ugly large :-). I’ll try to work with one big
induction proof now.

But thanks for the suggestion.

Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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