| commit | 4e56330e2f65e7f8e4e7d21593b453d537d90e67 | |
| author | Tim Makarios <tjm1983@gmail.com> | |
| Thu, 2 Apr 2015 03:53:37 +0000 (2 16:53 +1300) | ||
| committer | Tim Makarios <tjm1983@gmail.com> | |
| Thu, 2 Apr 2015 03:53:37 +0000 (2 16:53 +1300) | ||
| tree | 588bfc66b0c087fa080ccb40144a239c2bc77295 | treesnapshot (tar.gz zip) |
| parent | f55a3d7a8f843638c36b617357e6489ba2752a2d | commitdiff |
Showed "inv f y = x" is equivalent to "f x = y" if "bij f" is true
| Miscellany.thy | diffblobblamehistory |