Conversation
|
LGTM, I think the test failures are not related to the changes introduced. |
|
@florian-rabe FYI this is coming from the student working on tetrapodal search. |
|
Why has this not been merged? Was this just forgotten? |
|
Which # is it? Is the # the bug or the fix? |
The # is the "bug" - Isabelle uses that (if I remember correctly) as a separator between a name and it's "declaration type"; e.g. "zero#constant", "Nat#type" etc. |
Is that a problem? I believe all this patch changes is the emitted namespace. Any more hashes afterwards in an URIs should not be a problem(?) The problem from what I understand is just that the namespace that's being emitted is missing the hash, so we get |
This patch fixes a typo in the XML namespace in the Isabelle exporter. If you look at the ontology file you see that the XML namespace ends with a hash.