#167 (Apr 25, 2016, 9:44:10 PM)

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

Started by an SCM change