[isabelle-dev] goals inserts facts into goal statement

[Makarius]

On Fri, 24 Jul 2015, Andreas Lochbihler wrote:

> I am trying to replace some of my old usages of case goal_* with the new 
> goals method. In the course, I encountered the problem that goal inserts the 
> facts chained in as additional assumptions of my goals and also for the case 
> bindings.

I've now changed that in 2a03ae772c60 -- it did not affect any of the 
existing uses so far.

In 5976fe402824, I have renamed "goals" to "goal_cases" to emphasize its 
meaning.

The main Isabelle repository is already clear of "case goal42", with the 
exception of session HOL-IMP.


 	Makarius