This is the continuation / conclusion of the pending thread about flexflex
pairs in blast, see also
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-December/msg00085.html
In Isabelle/b45b1b217f43 from 01-Jan-2014 the smashing of flexflex pairs
is already removed, just like for
On 28 December, 2013 19:53 CET, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
HOL-Complex now builds with strict naming policy for facts (again).
Thanks, that's cool.
I have stumbled over something which needs some consideration: with
strict naming policy, locales can
