# Re: [isabelle] Isabelle2013-1-RC2 available for testing

Dear all,

`some (mostly unimportant) comments and questions on the extended
``documentation of the function package (nice to have the new elim/cases
``rules!):
`

`- "A definition of function f" -> "The definition of a function f"
``(Otherwise it sounds like only "f", and no other function, gives rise to
``the new rules.)
`

`- "also tell us" -> "also tells us" (Since "the rule", independent of
``its name, is singular.)
`

`- "elim rules above" -> "elims rule above" (?) (Why is "elim" typeset as
``it is? Should this refer to the name of the fact, or the "elim" attribute?)
`
- In the example lemma, how about the more "canonical"
lemma
assumes "list_to_option xs = y"
shows "P"
using assms
proof (rule list_to_option.elims)
fix x
assume "xs = [x]" and "y = Some x"
then show "P" sorry
next
assume "xs = []" and "y = None"
then show "P" sorry
next
fix a b xs'
assume "xs = a # b # xs'" and "y = None"
then show "P" sorry
qed
instead of using the old-school "erule"?

`- In general, why is the name "f.elims" (rather than "f.elim")? Won't
``this be a single rule in most cases? Only for mutually recursive
``functions there are more? Or do I miss something? (Sorry if this was
``discussed before.)
`

`- Btw: A few words on what happens for mutually recursive functions
``might be helpful (e.g., with the "standard" definition of "even"/"odd" I
``end up with 3 rules in each of "even.elims" and "odd.elims").
`
cheers
chris

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