Shifting the focus

In order to inspect or execute another refinement, e.g. <#54#>start horses<#54#>, we have to shift the focus by means of the focus-command


#elan55#

We can now inspect this refinement by means of the show-command. The focus-command (<#57#>f<#57#>) can be used to focus on any name, be it already defined or unknown. For focussing on known names, a shorthand mechanism exists: we may replace the last part of the name by a <#58#>*<#58#>, e.g.


#elan59#

Notice that if we had given a shorter part of the name <#61#>start*;SPMlt;RET;SPMgt;<#61#> we would have obtained the object <#62#>start pos<#62#> instead.