Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"



thm hd_def gives information on where to look, but that theory file (SList.thy) is apparently only for "historical interest".

It seems that you grepped for "list_rec", but the list_rec combinator mentioned in hd_def is generated internally by the datatype package, so it is not defined explicitly in a theory. The list_rec in SList.thy is unrelated.

Alex





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