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