Changes

Summary

1. more checks;
2. clarified message;
3. clarified message;
4. clarified comments;
5. clarified message;
6. improved list_neq simproc
7. merged
8. repaired document
9. merged
10. merged
11. A couple of basic lemmas about arg
12. multiset as equivalence class of permuted lists
13. emphasize connection to multisets
14. proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;
15. more on Isabelle_System.bash;
16. more specific name
17. more lemmas
18. dropped obscure FIXME
19. proper usage of hypotheses for zipperposition's TPTP generation
20. merged
21. tuned Mirabelle to parse option check_trivial only once
22. merged
23. merged
24. added stride option to Mirabelle
25. proper prover capabilities for zipperposition
26. NEWS;
27. merged
28. clarified uses of Isabelle_System.bash_process: more checks, fewer messages;
29. tuned signature;
30. more direct timing from bash_process wrapper;
31. tuned;
32. clarified signature, following Isabelle/Scala;
33. tuned;
34. clarified signature;
35. clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;
36. clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
37. tuned;
38. clarified signature, following Isabelle/Scala;
39. tuned signature;
40. clarified signature: process_result timing from Isabelle/Scala;
41. NEWS
42. dedicated locale for preorder and abstract bdd operation
43. get rid of traditional predicate
44. proper treatment of process_result;
45. more accurate process_result in ML, corresponding to Process_Result in Scala;
46. clarified: proper trim_line for error;
47. unused;
48. clarified lines (again);
49. clarified modules;
50. more uniform Bash.process: always ask Isabelle/Scala;
51. more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);
52. clarified compiler options;
53. tuned comments;
54. removed obsolete RC tags;

Summary

1. merge from afp-2021
2. revert accidental change
3. merge from afp-2021
4. website update
5. fix typo (Bauer -> Bayer)
6. new entry BTree
7. add Windows example to use-instructions
8. Isabelle app layout changed on Mac
9. Formal_Puiseux_Series website
10. new entry Formal_Puiseux_Series
11. 2021 web pages
12. update with 2021 release .tar.gz's
13. add Isabelle2021 release date
14. update .tar.gz releases
15. set version to 2021
16. multiset as equivalence class of permuted lists
17. emphasize connection to multisets
18. more specific name
19. merged
20. adapted to Isabelle/0110e2e2964c;
21. adapted to Isabelle/f0db1e4c89bc;
22. dedicated locale for preorder and abstract bdd operation
23. get rid of traditional predicate
24. more accurate process_result;
25. adapted to Isabelle/440546ea20e6;