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]]
Peter Lammich schrieb:
> Hi all,
> the reference manual says:
> "The configuration option depth limit limits the number of recursive
> 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]
This archive was generated by a fusion of
Pipermail (Mailman edition) and