[isabelle] strong and weak premises



Hi,

in the Isar 2016 slides, strong and weak premises are shown:

strong premises: have B if A1 and A2

weak premises: have B when A1 and A2

but they are not explained in details.

What does

   show A1 ==> A2 ... ==> B becomes free for re-interpretation
   so these are strong premises

mean?

- Gergely



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.