[examples] Replace all raw HTML `<details>` by `[[details]]`
It works like this
// [[details]] includes
// [[/details]]
automatically expands to
// <details><summary> Click to show includes </summary>
// </details>
This assures that we have "unified descriptions" and don't use that much raw html in the docs.
Edited by Timo Koch