Skip to content

Type classes for updates properties

Jacques-Henri Jourdan requested to merge jh/generic_updates into gen_proofmode

IT turns out that iGPS and alike also need basic and fancy updates, and their properties are very similar (that is, apart from the properties relating them to ownership, they have exactly the same theory). Hence, a lot of proofs and instances can be shared across the several logics.

Merge request reports