[isabelle-dev] NEWS: discontinued old-style goal cases

Makarius makarius at sketis.net
Sun Sep 23 23:10:57 CEST 2018

*** Isar ***

* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).

This refers to 8c240fdeffcb. The NEWS for Isabelle2016 already explain
that the proof method "goal_cases" is the proper way to do it.


More information about the isabelle-dev mailing list