# HG changeset patch
# User wenzelm
# Date 1615320665 -3600
# Node ID 299f6a8faccc3d35350894ca9b7204add7fa4015
# Parent  e19cb4c114093633a08ddde7325afe836012b410
proper type-setting of cartouches (requires T1);
\usepackage[T1]{fontenc} is default for mkroot;
\usepackage[utf8]{inputenc} is obsolete in lualatex;

diff -r e19cb4c11409 -r 299f6a8faccc NEWS
--- a/NEWS	Tue Mar 09 20:00:44 2021 +0100
+++ b/NEWS	Tue Mar 09 21:11:05 2021 +0100
@@ -17,6 +17,13 @@
 in boundary cases.
 
 
+*** Document preparation ***
+
+* More accurate LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
+\guilsinglright. Minor INCOMPATIBILITY, use \usepackage[T1]{fontenc}
+(which is now also the default in "isabelle mkroot").
+
+
 *** HOL ***
 
 * Theory Multiset: dedicated predicate "multiset" is gone, use
diff -r e19cb4c11409 -r 299f6a8faccc lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue Mar 09 20:00:44 2021 +0100
+++ b/lib/texinputs/isabelle.sty	Tue Mar 09 21:11:05 2021 +0100
@@ -112,8 +112,8 @@
 \chardef\isachartilde=`\~%
 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
-\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacartoucheopen{\isatext{\guilsinglleft}}%
+\def\isacartoucheclose{\isatext{\guilsinglright}}%
 }
 
 
@@ -205,8 +205,8 @@
 \def\isacharbar{\isamath{\mid}}%
 \def\isacharbraceright{\isamath{\}}}%
 \def\isachartilde{\isamath{{}\sp{\sim}}}%
-\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
+\def\isacharbackquoteclose{\isatext{\guilsinglright}}%
 }
 
 \newcommand{\isabellestyleliteral}{%
diff -r e19cb4c11409 -r 299f6a8faccc lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Tue Mar 09 20:00:44 2021 +0100
+++ b/lib/texinputs/isabellesym.sty	Tue Mar 09 21:11:05 2021 +0100
@@ -364,8 +364,8 @@
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
-\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
-\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymopen}{\isatext{\guilsinglleft}}
+\newcommand{\isasymclose}{\isatext{\guilsinglright}}
 \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
diff -r e19cb4c11409 -r 299f6a8faccc src/CTT/document/root.tex
--- a/src/CTT/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/CTT/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/Doc/Functions/document/root.tex
--- a/src/Doc/Functions/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/Doc/Functions/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,6 +1,5 @@
-
 \documentclass[a4paper,fleqn]{article}
-
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{iman,extra,isar}
diff -r e19cb4c11409 -r 299f6a8faccc src/FOL/document/root.tex
--- a/src/FOL/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/FOL/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/FOL/ex/document/root.tex
--- a/src/FOL/ex/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/FOL/ex/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Algebra/document/root.tex
--- a/src/HOL/Algebra/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Algebra/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,9 +1,8 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage{textcomp}
-\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{amsmath}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Analysis/document/root.tex
--- a/src/HOL/Analysis/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Analysis/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Auth/document/root.tex
--- a/src/HOL/Auth/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Auth/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{amssymb}
 \usepackage{textcomp}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Cardinals/document/root.tex
--- a/src/HOL/Cardinals/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Cardinals/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % this should be the last package used
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Complex_Analysis/document/root.tex
--- a/src/HOL/Complex_Analysis/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Complex_Analysis/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Data_Structures/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 \usepackage{amssymb}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Examples/document/root.tex
--- a/src/HOL/Examples/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Examples/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,6 +1,5 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/HOLCF/IMP/document/root.tex
--- a/src/HOL/HOLCF/IMP/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/HOLCF/IMP/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{textcomp}
 \usepackage{pdfsetup}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/HOLCF/document/root.tex
--- a/src/HOL/HOLCF/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/HOLCF/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,7 +1,5 @@
-
-% HOLCF/document/root.tex
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{textcomp}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Hahn_Banach/document/root.tex
--- a/src/HOL/Hahn_Banach/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Hahn_Banach/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Homology/document/root.tex
--- a/src/HOL/Homology/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Homology/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/IMP/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 % this should be the last package used
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Induct/document/root.tex
--- a/src/HOL/Induct/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Induct/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{amssymb}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 \isabellestyle{it}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Lattice/document/root.tex
--- a/src/HOL/Lattice/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Lattice/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym,pdfsetup}
 \usepackage[only,bigsqcap]{stmaryrd}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Library/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{ifthen}
-\usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
 \usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
 \usepackage{isabelle,isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Matrix_LP/document/root.tex
--- a/src/HOL/Matrix_LP/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Matrix_LP/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % this should be the last package used
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/MicroJava/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
 
 \urlstyle{rm}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/NanoJava/document/root.tex
--- a/src/HOL/NanoJava/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/NanoJava/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,latexsym,pdfsetup}
 
 \urlstyle{tt}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Nonstandard_Analysis/document/root.tex
--- a/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath,amssymb}
 \usepackage{stmaryrd}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Number_Theory/document/root.tex
--- a/src/HOL/Number_Theory/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Number_Theory/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Probability/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,10 +1,10 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{wasysym}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 \usepackage[english]{babel}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Proofs/Extraction/document/root.tex
--- a/src/HOL/Proofs/Extraction/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Proofs/Extraction/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Real_Asymp/Manual/document/root.tex
--- a/src/HOL/Real_Asymp/Manual/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Real_Asymp/Manual/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{amsfonts, amsmath, amssymb}
 \usepackage{railsetup}
 \usepackage{iman}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/SET_Protocol/document/root.tex
--- a/src/HOL/SET_Protocol/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/SET_Protocol/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/SPARK/Manual/document/root.tex
--- a/src/HOL/SPARK/Manual/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/SPARK/Manual/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[12pt,a4paper]{report}
-
+\usepackage[T1]{fontenc}
 \usepackage[a4paper,hscale=0.65,vscale=0.71]{geometry}
 
 \usepackage{isabelle,isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Statespace/document/root.tex
--- a/src/HOL/Statespace/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Statespace/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 % this should be the last package used
 \usepackage{pdfsetup}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/UNITY/document/root.tex
--- a/src/HOL/UNITY/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/UNITY/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/Unix/document/root.tex
--- a/src/HOL/Unix/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/Unix/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
 %for best-style documents ...
diff -r e19cb4c11409 -r 299f6a8faccc src/HOL/document/root.tex
--- a/src/HOL/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/HOL/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,11 +1,11 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{textcomp}
 \usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r e19cb4c11409 -r 299f6a8faccc src/Pure/Examples/document/root.tex
--- a/src/Pure/Examples/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/Pure/Examples/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,6 +1,5 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
 \isabellestyle{literal}
diff -r e19cb4c11409 -r 299f6a8faccc src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/Pure/Tools/mkroot.scala	Tue Mar 09 21:11:05 2021 +0100
@@ -71,6 +71,7 @@
 
       File.write(root_tex,
 """\documentclass[11pt,a4paper]{article}
+\""" + """usepackage[T1]{fontenc}
 \""" + """usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
diff -r e19cb4c11409 -r 299f6a8faccc src/ZF/AC/document/root.tex
--- a/src/ZF/AC/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/ZF/AC/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,amssymb,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}
diff -r e19cb4c11409 -r 299f6a8faccc src/ZF/Constructible/document/root.tex
--- a/src/ZF/Constructible/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/ZF/Constructible/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,amssymb,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}
diff -r e19cb4c11409 -r 299f6a8faccc src/ZF/IMP/document/root.tex
--- a/src/ZF/IMP/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/ZF/IMP/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[a4wide]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r e19cb4c11409 -r 299f6a8faccc src/ZF/Induct/document/root.tex
--- a/src/ZF/Induct/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/ZF/Induct/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,7 +1,7 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r e19cb4c11409 -r 299f6a8faccc src/ZF/document/root.tex
--- a/src/ZF/document/root.tex	Tue Mar 09 20:00:44 2021 +0100
+++ b/src/ZF/document/root.tex	Tue Mar 09 21:11:05 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym}
 \usepackage{amssymb}
 \usepackage[english]{babel}