Changes

Summary

1. merged
2. update documentation on simproc_setup;
3. tuned;
4. proper morphism;
5. simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
6. more compact ML source;
7. more robust read_simproc_spec: proper error positions;
8. tuned signature;
9. more standard simproc_setup using ML antiquotation;
10. more standard simproc_setup using ML antiquotation;
11. more standard simproc_setup using ML antiquotation;
12. added ML antiquotation "simproc_setup";
13. clarified signature;
14. clarified signature; clarified modules;
15. tuned signature;
16. tuned signature;
17. clarified signature;
18. clarified syntax and order of parameters;
19. clarified signature: Named_Target.setup works both for global and local theory;
20. clarified signature; clarified modules;
21. clarified signature: more concise simproc setup in ML;
22. clarified signature: more concise variations on implicit theory setup;
23. clarified simproc_setup (passive);
24. clarified 'simproc_setup';
25. support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
26. more standard simproc_setup in Isar; recovered examples from dead comments;
27. more standard ML setup; proper tracing messages depending on context option, not Unsynchronized.ref; tuned whitespace;