[isabelle-dev] NEWS: literal facts
makarius at sketis.net
Mon Jul 4 21:30:32 CEST 2016
* 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.
More information about the isabelle-dev