?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
blame | history | raw | HEAD
Explanatory comments about the definitions of learnable and constructible
[rttp-proofs.git] / RTTP.thy
blob4c06a4dd7fe22831c6c9b65e53b44f46937f5f49
1 header {* Responsible Trust Traversal Protocol *}
2 theory RTTP
3 imports
4   Main
5   Communication
6 begin
7 end
This is intended to be a computer-verifiable (but somewhat human-readable) collection of proofs that RTTP has certain properties.