In typing statements of a proof into an Isabelle (2020) theory file, e.g.,
from ?prime p ? have p: "1 < p "
the jEdit interface application pops up a tooltip offering to insert an open cartouche command <open>
when I type a quotation mark. As you can see in the line above, I have been allowing this and it seems to be permitted. The Isabelle documentation seems to view inner syntax as category embedded, which seems to permit delineation with quotation marks or with the cartouche enclosure <open ... <close>.
Is there a down side to doing this? The imports
statement requires quoting a reference to a theory file "HOL-Computational_Algebra.Primes" with module.theory format and will not accept cartouche there, but in theory statements it certainly appears to be equivalent.