Allow creation of subgoals in non-local scope

[GoogleCodeExporter]

At the moment, most refinements (e.g. relabelling, elimination) cause the 
context to become gradually more cluttered as many unnecessary things come into 
scope. We need a standard way to refine a problem without duplicating things in 
scope.

We should be able to create a subgoal above part of the local context 
(initially by providing a list of parameters to escape from, but perhaps later 
using a proper cursor). We could then realise the current goal from the subgoal 
appropriately. This would allow more relabelling to be more principled and 
elimination to avoid generating a huge context.

Original issue reported on code.google.com by adamgundry on 3 Sep 2010 at 3:22

[GoogleCodeExporter]

I've pushed a bunch of patches (marked issue 77) that solve the problem in a 
slightly different way: refinements always create subgoals at the top of the 
current development, and re-abstract over any parameters within it. This means 
relabelling really works properly (it changes the name advice in the 
programming problem display) and the context expansion problem is kept under 
control.

Original comment by adamgundry on 13 Sep 2010 at 8:14

• Changed state: Fixed