On Mon, 22 Oct 2012, Florian Haftmann wrote:
I first thought it would be related to 1167c1157a5b (haftmann on
src/Pure/Proof/extraction.ML), which is not immediately easy to follow
in every detail.
It indeed isn't, but the effect is idempotent.
To my defence, reordering arguments is not very comprehensible from a diff.
In such cases, the general question is if making the sources "canonical"
has any purpose. It is rather old material by Stefan Berghofer, written
in the typical style from around 2000, and not going to be revisited in
the foreseeable future. There are no fundamental known problems with it.
So why change it in the first place?
Concerning the digestability of the changeset, it did not turn out as bad
as first anticipated. Bitbucket has pretty good word-wise diffs. So
after spending about 45min with:
https://bitbucket.org/makarius/isabelle/changeset/1167c1157a5b83b05bd259adb7ee9b7729d98303
I came to the conclusion that the changeset is clean.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
