--- a/NEWS Tue Apr 20 22:53:24 2021 +0200
+++ b/NEWS Thu Apr 22 10:11:11 2021 +0200
@@ -33,6 +33,10 @@
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").
+* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
+\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
+no longer required.
+
*** HOL ***
--- a/lib/texinputs/isabellesym.sty Tue Apr 20 22:53:24 2021 +0200
+++ b/lib/texinputs/isabellesym.sty Thu Apr 22 10:11:11 2021 +0200
@@ -234,8 +234,8 @@
\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}}
\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}}
\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
+\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}}
+\newcommand{\isasymguillemotright}{\isatext{\guillemotright}}
\newcommand{\isasymbottom}{\isamath{\bot}}
\newcommand{\isasymtop}{\isamath{\top}}
\newcommand{\isasymand}{\isamath{\wedge}}
--- a/src/Doc/Nitpick/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/Doc/Nitpick/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage{color}
\usepackage{footmisc}
\usepackage{graphicx}
@@ -32,7 +31,7 @@
\def\undef{(\lambda x.\; \_)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
--- a/src/Doc/Sledgehammer/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage{color}
\usepackage{footmisc}
\usepackage{graphicx}
@@ -40,7 +39,7 @@
\def\undef{(\lambda x.\; \unk)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
\urlstyle{tt}
--- a/src/Doc/Tutorial/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/Doc/Tutorial/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -3,7 +3,6 @@
\usepackage{proof,amsmath,amsfonts,amssymb}
\usepackage{wasysym,verbatim,graphicx,tutorial,ttbox,comment}
\usepackage{eurosym}
-\usepackage[english]{babel}
\usepackage{pdfsetup}
%last package!
--- a/src/HOL/Bali/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Bali/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -4,7 +4,6 @@
\usepackage{latexsym}
\usepackage{graphicx}
\usepackage{pdfsetup}
-\usepackage[english]{babel}
\usepackage{ifthen}
\urlstyle{rm}
--- a/src/HOL/Hoare/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Hoare/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Hoare_Parallel/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Hoare_Parallel/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -1,6 +1,6 @@
\documentclass[11pt,a4paper]{report}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Imperative_HOL/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Imperative_HOL/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -1,7 +1,6 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx,isabelle,isabellesym,latexsym}
\usepackage{amssymb}
-\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
\usepackage{ifthen}
--- a/src/HOL/Library/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Library/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -1,7 +1,6 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{ifthen}
-\usepackage[english]{babel}
\usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
--- a/src/HOL/Probability/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Probability/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -6,7 +6,6 @@
\usepackage{wasysym}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
-\usepackage[english]{babel}
\urlstyle{rm}
\isabellestyle{it}
--- a/src/HOL/Proofs/Lambda/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/Proofs/Lambda/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -1,7 +1,7 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
\usepackage{graphicx}
-\usepackage[english]{babel}
\usepackage{amssymb}
\usepackage{textcomp}
\usepackage{isabelle,isabellesym,pdfsetup}
--- a/src/HOL/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/HOL/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -4,7 +4,6 @@
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{textcomp}
-\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{pdfsetup}
--- a/src/ZF/document/root.tex Tue Apr 20 22:53:24 2021 +0200
+++ b/src/ZF/document/root.tex Thu Apr 22 10:11:11 2021 +0200
@@ -2,7 +2,6 @@
\usepackage[T1]{fontenc}
\usepackage{graphicx,isabelle,isabellesym}
\usepackage{amssymb}
-\usepackage[english]{babel}
% this should be the last package used
\usepackage{pdfsetup}