Changes

Summary

1. deleting a code equation never leads to unimplemented function
2. avoid ancient [code, code del] antipattern
3. obsolete
4. register equations stemming from extracted proofs as specification rules
5. tuned
6. merged
7. tuned signature;
8. proper treatment of empty result;
9. clarified modules;
10. tuned signature;
11. provide spell-checker menu via completion commands;
12. added commands for spell-checker dictionary;
13. tuned signature;
14. tuning
15. SMT news
16. correctly unfold applied 'let's (e.g. '(let x = a in f) b') -- and removed dead code
17. do not print unimplemented functions
18. dropped void values
19. more uniform order of constructors
20. more consistent terminology
21. avoid name particle "the" where no selection is implied
22. more uniform ordering and naming of sections; proper local function
23. tuned internal signature
24. more explicit constructor name
25. tuned whitespace
26. replaced recdef by fun
27. spelling