[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.