On 26.01.2015 20:12, Makarius wrote:
> On Wed, 21 Jan 2015, Lars Noschinski wrote:
>
>> While the UI was clearly subobtimal, I found it very useful to be able
>> to show only a part of the total graph (via "Show -> only children" or
>> so). Similarly, I liked the ability to highlight the children/p
See now 0a528e3aad28 and d3f4ddeaacc3 for the critical changes.
Producing correct and readable patterns is a challenge and,
unfortunately but necessarily, happens mostly without any backing from
the inference kernel. Future work with more semantic foundations might
bring progress here.
F
> My conclusion of this discussion is that with 8fab871a2a6f the sublocale
> command immediately visits its target after the qed, which it didn't before.
> This now causes the command to loop. Is this correct?
Yes, definitely.
Florian
--
PGP available:
http://home.informatik.tu-mue
