[isabelle] depth_limit for simplifier



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.