# HG changeset patch
# User nipkow
# Date 1639039215 -3600
# Node ID 7dbac7d3cdab3a95479310e48b457e65d1bbc514
# Parent  1c50ddcf6a01200d2cfe187ebec4236a90306d00
missing latex font

diff -r 1c50ddcf6a01 -r 7dbac7d3cdab src/HOL/Examples/Rewrite_Examples.thy
--- 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>
diff -r 1c50ddcf6a01 -r 7dbac7d3cdab src/HOL/Examples/document/root.tex
--- 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}