On 28 December, 2013 19:53 CET, Florian Haftmann
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 be compromised by »injecting«
> duplica
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 any
