[isabelle-dev] goals inserts facts into goal statement
makarius at sketis.net
Mon Sep 14 11:40:21 CEST 2015
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
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
The main Isabelle repository is already clear of "case goal42", with the
exception of session HOL-IMP.
More information about the isabelle-dev