• David Swasey's avatar
    Combine `Atomic e` and `StronglyAtomic e` into `Atomic s e` and introduce `HeadAtomic s e`. · 7dc00c5f
    David Swasey authored
    I saw no need for `stuckness_flip`: strong atomicity always works,
    while weak atomicity works only for expressions that are not stuck.
    Since this seemed unclear, I split lemma `wp_atomic'` up into
    `wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic`
    (not). The proof mode instance is stated in terms of the derived rule
    `wp_atomic` (parametric in `s`).
    7dc00c5f
lifting.v 7.34 KB