[isabelle-dev] NEWS

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Fri Oct 9 09:04:37 CEST 2015

Dear Ondrej,

Thanks a lot for this. Now I can scrap my own semi-working debugging infrastructure for 

Just a comments: Can you add a flag to transfer_step such that it outputs the rule it used 
as tracing information? My problem is that with big terms, I get a lot of subgoals (> 50). 
If I try to identify missing rules, I check the replacement of the current term in the 
skeleton, but as the skeleton is the last goal, I have to increase the limit of goal 
states and always scroll down in the output panel. Now if I could see the rule directly in 
the output buffer, I could see there directly when something goes wrong.


On 09/10/15 01:52, Ondřej Kunčar wrote:
> * Transfer:
>    - new methods for interactive debugging of 'transfer' and
>      'transfer_prover': 'transfer_start', 'transfer_step',
>      'transfer_end', 'transfer_prover_start'
>      and 'transfer_prover_end'.
> This refers to 46af4f577c7e.
> See the Isar Reference Manual and the example file "~~/src/HOL/ex/Transfer_Debug.thy".
> Ondrej
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list