Shifting the focus

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


#litout508#

We can now inspect this refinement by means of the show-command. The focus-command (<#358#>f<#358#>) 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 <#359#>*<#359#>, e.g.


#litout510#

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