Skip to content

provide a lemma to update only the authoritative part, ignoring the fragments entirely

Ralf Jung requested to merge ralf/update into master

Surprisingly, I could not find a transitivity lemma for updates either, so I added one.

Merge request reports