?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: 1779f6a) | patch
Proved that "events_before h t" is monotonic in t
commitaf31651461702071ec32401b760252fb27b9048d
authorTim Makarios <tjm1983@gmail.com>
Tue, 16 Jun 2015 04:51:00 +0000 (16 16:51 +1200)
committerTim Makarios <tjm1983@gmail.com>
Tue, 16 Jun 2015 04:51:00 +0000 (16 16:51 +1200)
treec812886259207ae4d03064cac3e5b0b931149dcetree | snapshot (tar.gz zip)
parent1779f6a685454b719146e78bedc4810b4d847d7dcommit | diff
Proved that "events_before h t" is monotonic in t
Communication.thy diff | blob | blame | history
This is intended to be a computer-verifiable (but somewhat human-readable) collection of proofs that RTTP has certain properties.