Changes

Summary

1. clarified rendering;
2. old 'def' is legacy;
3. more rigid check of lhs;
4. clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
5. eliminated old 'def'; tuned comments;
6. added Isar command 'define';
7. within a proof body context, undeclared frees are like global constants; tuned signature;
8. clarified modules;