diff options
| author | Tanaka Akira | 2019-01-31 16:12:25 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:12:25 +0900 |
| commit | ddcd0afd740278b7b18999cd8ad4aa01c8b26d5f (patch) | |
| tree | a9e4748d9ddee97800d8d4183ae938822227a4e7 /doc/plugin_tutorial/tuto1/src/simple_print.ml | |
| parent | 4f42fb583275bab31eab93c58c0cdd547c51d990 (diff) | |
Use \Prop, \Set and \Type defined in refman-preamble.sty.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_print.ml')
0 files changed, 0 insertions, 0 deletions