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 unfol
(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
