[isabelle-dev] NEWS: literal facts

Makarius 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 mailing list