diff options
| author | Pierre-Marie Pédrot | 2014-03-28 14:51:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-28 14:53:54 +0100 |
| commit | 863b9a54e58b9548dd4691d3864b3e6cda9e63a0 (patch) | |
| tree | d7d2f74277f96e5321b1cf18d508789546cd08a1 /dev/base_include | |
| parent | 91eb9e8cd5c68d5a71c07787900a8bb6d0481ba9 (diff) | |
Using the new refine interface to define ML tactics.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions