?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: f80f1cf) | patch
Proved constructed_from_not_received_implies_constructedmaster
commit1ce834c565fe9ac43ee781626fd3c42d27980265
authorTim Makarios <tjm1983@gmail.com>
Fri, 19 Jun 2015 00:55:55 +0000 (19 12:55 +1200)
committerTim Makarios <tjm1983@gmail.com>
Fri, 19 Jun 2015 00:55:55 +0000 (19 12:55 +1200)
treef86d0683958564cbf99510d1683ef3c0a9c6f822tree | snapshot (tar.gz zip)
parentf80f1cfe895ccc9c0c7327150f3550e7243225b1commit | diff
Proved constructed_from_not_received_implies_constructed
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.