Public Git Hosting - rttp-proofs.git/commit

summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: 4d21858) | patch

commit	cd2815a3bfe4a586673e9df278afce8d9fa7dc1a
author	Tim Makarios <tjm1983@gmail.com>
	Tue, 20 Jan 2015 23:56:19 +0000 (21 12:56 +1300)
committer	Tim Makarios <tjm1983@gmail.com>
	Tue, 20 Jan 2015 23:56:19 +0000 (21 12:56 +1300)
tree	4f04fa5380a61c9013e55c32792ed399d9f16567	tree \| snapshot (tar.gz zip)
parent	4d21858258ec4708664099a2796e477831510662	commit \| diff

Inductive definition of constructible messages

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.