Changes

Summary

1. clarified zproof storage: per-theory table in anticipation of session exports;
2. proper thm_name for stored zproof;
3. uniform treatment of lazy facts: actual proof terms are always strict;
4. tuned;
5. tuned whitespace;
6. tuned;