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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and