proper type-setting of cartouches (requires T1);
\usepackage[T1]{fontenc} is default for mkroot;
\usepackage[utf8]{inputenc} is obsolete in lualatex;

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

--- 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}{%

--- 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---}}

--- 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}
 

--- 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}

--- 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}
 

--- 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}
 

--- 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}
 

--- 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}

--- 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}

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

--- 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}

--- 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}

--- 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}
 

--- 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}

--- 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}

--- 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}

--- 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}

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

--- 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}
 

--- 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}

--- 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}
 

--- 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}

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

--- 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}

--- 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}

--- 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}

--- 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}

--- 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}
 

--- 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}
 

--- 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}

--- 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}

--- 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}

--- 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}

--- 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}

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

--- 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}

--- 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}

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

--- 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}

--- 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}

--- 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}
 

--- 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}

--- 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}