diff options
| author | Thomas Bauereiss | 2018-12-18 14:59:59 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-12-18 15:08:34 +0000 |
| commit | 07a332c856b3ee9fe26a9cd47ea6005f9d579810 (patch) | |
| tree | 3d798c8786f91219be95c29312baaf2993800e66 /src/gen_lib | |
| parent | e5d108332cf700f73ea7b7527d0ae6006b0944c5 (diff) | |
Check more carefully for recursive functions when generating Lem
Annotating non-recursive functions as recursive in Lem output is
allowed, but will make Lem use "fun"/"function" commands when generating
Isabelle output, which is much slower to process than "definiton".
Diffstat (limited to 'src/gen_lib')
0 files changed, 0 insertions, 0 deletions