diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-01-30 18:43:26 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-01-30 22:19:21 +0100 |
| commit | 99b61a6ea3e7c9c96022ac7d573b10b2366e5c16 (patch) | |
| tree | 3f47e6e88891a4377d8b1062c656dc495d616beb /doc/refman | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
Proof clean-up.
- Do not use induction/elim when not necessary: use destruct or
destructive intro-pattern instead.
- Do not use heavy automation when lightweight automation is enough.
- Prefer shorter proofs when it does not hinder readability.
- Do not rely on automatically generated names.
- Use bullets.
Diffstat (limited to 'doc/refman')
0 files changed, 0 insertions, 0 deletions