wenzelm [Fri, 10 Jan 2014 21:37:28 +0100] rev 54984
more elementary management of declared hyps, below structure Assumption;
Goal.prove: insist in declared hyps;
Simplifier: declare hyps via Thm.assume_hyps;
more accurate tool context in some boundary cases;