diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 03:01:40 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:06:37 -0400 |
| commit | f52e7e152e37000d081470f73786ccdd9167f1c0 (patch) | |
| tree | afd4002b0c325ab380d7ac83280d9e435273e7ef /doc/plugin_tutorial | |
| parent | ec60835e6a41f368c1a91d4eac8c99e1853a2abc (diff) | |
[lemmas] Use direct-style for mutual lemma declaration.
Steps towards unification with `DeclareDef` API.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions