> BTW, you can also use completion on the theory base name, e.g. text > "Operational" followed by C+b in Isabelle/jEdit.
Thanks for your prompt help. I'm sorry about this mess-up. The version with an underscore existed in some patch, which I had popped to update the AFP. I had completely forgotten about that and thought the problem came from elsewhere. Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
