* Command 'case' allows fact name and attribute specification like this:
case a: (c xs)
case a [attributes]: (c xs)
Facts that are introduced by invoking the case context are uniformly
qualified by "a"; the same name is used for the cumulative fact. The old
form "case (c xs) [attributes]" is no longer supported. Rare
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
and always put attributes in front.
This refers to Isabelle/b7ee41f72add.
The inability to name the case facts was just a very old omission that
never got beyond a certain critical mass of pain to do something about it.
After seeing too many "case 1", "case 2", "case 3" and corresponding facts
"1", "2", "3" I've now pushed this trivial change through, really with
rare incompatibilities. (See also AFP/16e7d42ef7f4.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
