Re: [isabelle] strong and weak premises
On Fri, 5 Feb 2016, Buday Gergely wrote:
strong premises: have B if A1 and A2
weak premises: have B when A1 and A2
but they are not explained in details.
show A1 ==> A2 ... ==> B becomes free for re-interpretation
so these are strong premises
There is a bit more text in the isar-ref manual and the NEWS, notably:
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
The meaning of 'show' with Pure rule statements has changed: premises
are treated in the sense of 'assume', instead of 'presume'.
Weak premises are relatively unexciting and rarely used in practice. The
change means that typical accidents by beginners with show "A ==> B" do
not lead to unexpected results and disrupt the process of learning Isar.
In the rare situations where the weak form is intended, the explicit
'when' context may be used.
This archive was generated by a fusion of
Pipermail (Mailman edition) and