?  search:
summary | log | graphiclog1 | graphiclog2 | commit | commitdiff | tree | refs | edit | fork
(parent: 0f83bc3) | patch
Added "f (inv f x) = x" (when "bij f") as a simplification rule
commitf55a3d7a8f843638c36b617357e6489ba2752a2d
authorTim Makarios <tjm1983@gmail.com>
Thu, 2 Apr 2015 00:06:38 +0000 (2 13:06 +1300)
committerTim Makarios <tjm1983@gmail.com>
Thu, 2 Apr 2015 00:06:38 +0000 (2 13:06 +1300)
treee8259148d219035ab598ee6a495cbbb83c3a17a0tree | snapshot (tar.gz zip)
parent0f83bc34afc7c018e37cf473f9f3766d529661d8commit | diff
Added "f (inv f x) = x" (when "bij f") as a simplification rule
Miscellany.thy [new file with mode: 0644] blob
This is intended to be a computer-verifiable (but somewhat human-readable) collection of proofs that RTTP has certain properties.