# [isabelle] Induction rules of the function package

Hi all,

`the induction rules that the function package generates for a function
``definitions are usually great. However, is always quantifies over all
``parameters of the function, even if they are just passed through all
``recursive calls. For some proofs, I would like not to have them
``quantified. Is there an option to the function package to declare such
``parameters to treat differently (like the for clause for inductive)?
`
A concrete example:
fun map where
"map f [] = []"
| "map f (x # xs) = f x # map f xs"
produces the induction rule map.induct:
[| !!f. P f []; !!f x xs. P f xs ==> P f (x # xs) |] ==> P a0 a1

`but I would much more like the following rule (which I currently derive
``by hand from the generated one):
`[| P []; !!x xs. P xs ==> P (x # xs) |] ==> P a
Thanks,
Andreas

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