diff options
| author | Thomas Bauereiss | 2019-11-14 16:29:20 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-11-21 14:04:32 +0000 |
| commit | 8b9e89831df9227e1ac380573d36972449ddc408 (patch) | |
| tree | 971769c8b16d185f4fe113287408a278a54ad19d /src/specialize.ml | |
| parent | 1b27222cd06d824cf72d339d5acecf4d521ddd0f (diff) | |
Add option to generate grouped register state record
... with one field per register *type*, instead of one field per
register. The fields store functions from register name to value.
This leads to dramatically reduced processing time for the register
state record in HOL4.
Diffstat (limited to 'src/specialize.ml')
0 files changed, 0 insertions, 0 deletions