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