[isabelle-dev] NEWS: literal facts

[Makarius]

* The defining position of a literal fact ‹prop› is maintained more
carefully, and made accessible as hyperlink in the Prover IDE.

* Commands 'finally' and 'ultimately' used to expose the result as
literal fact: this accidental behaviour has been discontinued. Rare
INCOMPATIBILITY, use more explicit means to refer to facts in Isar.


This refers to Isabelle/8bbd325e89e6.


	Makarius