spec.het revision b3bacd257ffcdd346b70ab690f03b28ad5f33fdc
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder ded : o -> type.
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederspec SP = SP1 and SP2
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederspec SP' = SP then
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederplus : nat -> nat -> nat.
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder%view V1 : SP3 to SP4 = t |-> plus p p
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederspec SP5 = SP hide p
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder%spec SP6 = SP reveal i