--- a/src/HOL/Examples/Rewrite_Examples.thy Thu Dec 09 08:32:29 2021 +0100
+++ b/src/HOL/Examples/Rewrite_Examples.thy Thu Dec 09 09:40:15 2021 +0100
@@ -268,7 +268,7 @@
val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
\<close>
-section \<open>Regression tests\<close>
+text \<open>Some regression tests\<close>
ML \<open>
val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>
--- a/src/HOL/Examples/document/root.tex Thu Dec 09 08:32:29 2021 +0100
+++ b/src/HOL/Examples/document/root.tex Thu Dec 09 09:40:15 2021 +0100
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
+\usepackage{ifthen,proof,amssymb,isabelle,isabellesym,wasysym}
\isabellestyle{literal}
\usepackage{pdfsetup}\urlstyle{rm}