*** 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. Makarius