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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
