wenzelm [Fri, 02 Oct 2009 21:41:57 +0200] rev 32857
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;