<!DOCTYPE html>
<html lang="{{page.lang | default:"en"}}">
{% include head.html %}
<body>
{% include header.html %}
{{ content
| replace: '<!--qed-->', ' <span class=qed>∎</span>'
| replace: '\=\>', '⇒'
}}
{% include footer.html %}
{% include google_analytics.html %}
<!-- Page generated {{ site.time }} -->
<!-- Page ID {{ page.id }} -->
</body>
</html>