Re: [isabelle] depth_limit for simplifier

You currently have to do it via the Proof General settings menu.


Peter Lammich schrieb:
> Hi all,
> the reference manual says:
> "The configuration option depth limit limits the number of recursive
> invocations
> of the simplifier during conditional rewriting."
> However, there seems to be no documentation how to set this
> configuration option (?).
> How to set the depth-limit? Best would be locally just for one
> invokation of the simplifier, something like
>   apply (simp depth_limit=4)   [This does not work]
> Regards,
>   Peter

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