Can I use a custom qualifier name when importing a theory?
I'm looking for something like
theory Scratch
imports Very_Long_Name as foo
begin
(* I want to use foo.xxx *)
end
Pretty sure that's not possible. What you can do is locally define custom notation using e.g. the notation
command. Or abbreviation
, but I think abbreviations are more difficult to get rid of again.
There is also const_alias
, although I cannot comment much on that, as I have never used it.
Last updated: Jan 05 2025 at 16:21 UTC