?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: 00469e0) | patch
Proved that constructed_from is transitive
commit1779f6a685454b719146e78bedc4810b4d847d7d
authorTim Makarios <tjm1983@gmail.com>
Fri, 12 Jun 2015 04:40:58 +0000 (12 16:40 +1200)
committerTim Makarios <tjm1983@gmail.com>
Fri, 12 Jun 2015 04:40:58 +0000 (12 16:40 +1200)
tree57cb27f8ad1db193a4455eee3a0ec97e55e44d67tree | snapshot (tar.gz zip)
parent00469e0379a3e61346c3aa680b933acb1a211e55commit | diff
Proved that constructed_from is transitive
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.