# HG changeset patch
# User wenzelm
# Date 1619079071 -7200
# Node ID aece5cc9efb77f6ce5e7bb10ad32fc48bb8a1390
# Parent  e60333aa18cafe80545dc9b2c19ad746177c15b6
simplified typesetting of \<guillemotleft>...\<guillemotright>;

diff -r e60333aa18ca -r aece5cc9efb7 NEWS
--- 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 ***
 
diff -r e60333aa18ca -r aece5cc9efb7 lib/texinputs/isabellesym.sty
--- 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}}
diff -r e60333aa18ca -r aece5cc9efb7 src/Doc/Nitpick/document/root.tex
--- 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
diff -r e60333aa18ca -r aece5cc9efb7 src/Doc/Sledgehammer/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/Doc/Tutorial/document/root.tex
--- 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!
 
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Bali/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Hoare/document/root.tex
--- 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}
 
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Hoare_Parallel/document/root.tex
--- 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}
 
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Imperative_HOL/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Library/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Probability/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/Proofs/Lambda/document/root.tex
--- 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}
diff -r e60333aa18ca -r aece5cc9efb7 src/HOL/document/root.tex
--- 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}
 
diff -r e60333aa18ca -r aece5cc9efb7 src/ZF/document/root.tex
--- 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}