| #
4f781ce3 |
|
10-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix lisp_extractLib so its "definitions" retain "compute" attribute
It was storing theorems with names nm ^ "_def" and expecting these to
retain the "compute" attribute given to the original definition. As
per b98f5ead5, this is bogus and now longer works. The fix is just to
make the second call to save_thm also pass in the "compute" attribute.
|