| changeset 69045 | 8c240fdeffcb |
| parent 69044 | 364c989edb49 |
| child 69066 | 5f83db57e8c2 |
--- a/NEWS Sun Sep 23 21:38:30 2018 +0200 +++ b/NEWS Sun Sep 23 21:49:31 2018 +0200 @@ -18,6 +18,10 @@ * More robust treatment of structural errors: begin/end blocks take precedence over goal/proof. +* Implicit cases goal1, goal2, goal3, etc. have been discontinued +(legacy feature since Isabelle2016). + + *** HOL ***