(moved from isabelle-users since I'm referring to the development
versions of Isabelle and the AFP below)
Dear Julian,
unexpectedly I found some time to have a look earlier.
First, the naming layer provided by the lemmas statements in
Prefix_Order is there to keep compatibility with some AFP
Dear Christian,
Yes, I haven't considered AFP entries or anything, this was just my
personal hack to get it to work for my theories. I'll adjust the names
in my theories to whatever you see fit for Prefix_Order.
However, it seems like there is still an issue. The lemma
strict_prefixI gets
