Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014

Thank you very much.
I had a look at the news file but I guess I did not use the right search

>> (*) Why is "back" considered bad "style" (according to the AFP
>> submission guidelines)? I removed all occurrences in my code already but
>> I am still curious.
> Because it makes your proof rely on the order in which the HO-unifier
> produces its results.
This is what I also believed.
Why is it not required that back always produces an immediate fault,
i.e., always a unique result?
Without 'back' the first result is chosen but if the order changes, this
first element may be a different than before.

Remaining questions:
(*) In 2011 warnings were written to the response buffer. in
Isabelle2014/JEdit: is it possible to copy all these responses to a
certain file?

(*) Is it possible to adapt rename_tac s.t. it produces a warning if it
has not altered the state?

-- Sven Schneider

Attachment: 0xF0E2AE90.asc
Description: application/pgp-keys

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.