*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Induction rules of the function package*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 17 Sep 2009 10:38:36 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Hi Andreas,

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)?

Cheers, Alex

**Follow-Ups**:**Re: [isabelle] Induction rules of the function package***From:*Andreas Lochbihler

- Previous by Date: [isabelle] A finished project and an interesting unification bug
- Next by Date: Re: [isabelle] question about "fun"
- Previous by Thread: [isabelle] Induction rules of the function package
- Next by Thread: Re: [isabelle] Induction rules of the function package
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list