Re: [isabelle] Tips to make a simplification simpler?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Tips to make a simplification simpler?
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Thu, 02 Aug 2012 11:36:28 +0200
- In-reply-to: <op.wibgj5vsule2fv@douda-yannick>
- References: <op.wh9y1vs4ule2fv@douda-yannick> <5017765F.email@example.com> <op.wibgj5vsule2fv@douda-yannick>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.5) Gecko/20120624 Icedove/10.0.5
On 31.07.2012 17:13, Yannick Duchêne (Hibou57) wrote:
its tracing is stopped until it emerges from its recursive
invocations. This is
a very simpled-minded way of getting a abstract view of the trace. If
more tracing info, you can always increase the limit - in ProofGeneral
a menue item Trace Simplifier Depth for it.
I searched for a way to have the same with jEdit. That's the opportunity
of another topic.
You can do this by "using [[simp_trace_depth_limit=x]]"
This archive was generated by a fusion of
Pipermail (Mailman edition) and