Re: [isabelle] depth_limit for simplifier



Sorry, I was thinking of the Trace Simp Depth limit. What you want is

declare [[simp_depth_limit = 6]]

Tobias

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.