Make identifiers with capital letter global? #18
Description
Maybe when creating a nested namespace, the same way as we auto-import all numbers, we could auto-import all identifiers starting with a capital letter. That way we could rename functions and theorems to be like Replace_cut or Add_comm, so that we don't need to explicitly import them, but still have things like goal or a which are local and not imported to nested namespaces unless explicitly requested.