-
Ralf Jung authored
Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-condition
a8b812f9
Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-condition