# HG changeset patch
# User wenzelm
# Date 1616501611 -3600
# Node ID 2cc9bd9a735741f123fca1433a0fa83102a4dc8d
# Parent  41fc655585e401dfcfb871ef1c930f0427798604
discontinue fragile check in LaTeX, e.g. problems with toc entries;

diff -r 41fc655585e4 -r 2cc9bd9a7357 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Mon Mar 22 21:24:25 2021 +0000
+++ b/lib/texinputs/isabelle.sty	Tue Mar 23 13:13:31 2021 +0100
@@ -68,9 +68,6 @@
 \DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152}
 \DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153}
 \DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154}
-\newcommand{\checkbbbfont}{{%
-\setbox\@tempboxa=\hbox{$\bbbA$}%
-\ifdim\wd\@tempboxa=\z@\PackageError{isabelle/pxfonts}{Missing font txmia}{}\fi}}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
diff -r 41fc655585e4 -r 2cc9bd9a7357 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Mon Mar 22 21:24:25 2021 +0000
+++ b/lib/texinputs/isabellesym.sty	Tue Mar 23 13:13:31 2021 +0100
@@ -150,32 +150,32 @@
 \newcommand{\isasymPhi}{\isamath{\Phi}}
 \newcommand{\isasymPsi}{\isamath{\Psi}}
 \newcommand{\isasymOmega}{\isamath{\Omega}}
-\newcommand{\isasymbbbA}{\checkbbbfont\isamath{\bbbA}}  %requires font txmia from txfonts
-\newcommand{\isasymbool}{\checkbbbfont\isamath{\bbbB}}  %requires font txmia from txfonts
-\newcommand{\isasymcomplex}{\checkbbbfont\isamath{\bbbC}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbD}{\checkbbbfont\isamath{\bbbD}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbE}{\checkbbbfont\isamath{\bbbE}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbF}{\checkbbbfont\isamath{\bbbF}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbG}{\checkbbbfont\isamath{\bbbG}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbH}{\checkbbbfont\isamath{\bbbH}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbI}{\checkbbbfont\isamath{\bbbI}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbJ}{\checkbbbfont\isamath{\bbbJ}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbK}{\checkbbbfont\isamath{\bbbK}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbL}{\checkbbbfont\isamath{\bbbL}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbM}{\checkbbbfont\isamath{\bbbM}}  %requires font txmia from txfonts
-\newcommand{\isasymnat}{\checkbbbfont\isamath{\bbbN}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbO}{\checkbbbfont\isamath{\bbbO}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbP}{\checkbbbfont\isamath{\bbbP}}  %requires font txmia from txfonts
-\newcommand{\isasymrat}{\checkbbbfont\isamath{\bbbQ}}  %requires font txmia from txfonts
-\newcommand{\isasymreal}{\checkbbbfont\isamath{\bbbR}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbS}{\checkbbbfont\isamath{\bbbS}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbT}{\checkbbbfont\isamath{\bbbT}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbU}{\checkbbbfont\isamath{\bbbU}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbV}{\checkbbbfont\isamath{\bbbV}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbW}{\checkbbbfont\isamath{\bbbW}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbX}{\checkbbbfont\isamath{\bbbX}}  %requires font txmia from txfonts
-\newcommand{\isasymbbbY}{\checkbbbfont\isamath{\bbbY}}  %requires font txmia from txfonts
-\newcommand{\isasymint}{\checkbbbfont\isamath{\bbbZ}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbA}{\isamath{\bbbA}}  %requires font txmia from txfonts
+\newcommand{\isasymbool}{\isamath{\bbbB}}  %requires font txmia from txfonts
+\newcommand{\isasymcomplex}{\isamath{\bbbC}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbD}{\isamath{\bbbD}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbE}{\isamath{\bbbE}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbF}{\isamath{\bbbF}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbG}{\isamath{\bbbG}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbH}{\isamath{\bbbH}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbI}{\isamath{\bbbI}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbJ}{\isamath{\bbbJ}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbK}{\isamath{\bbbK}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbL}{\isamath{\bbbL}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbM}{\isamath{\bbbM}}  %requires font txmia from txfonts
+\newcommand{\isasymnat}{\isamath{\bbbN}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbO}{\isamath{\bbbO}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbP}{\isamath{\bbbP}}  %requires font txmia from txfonts
+\newcommand{\isasymrat}{\isamath{\bbbQ}}  %requires font txmia from txfonts
+\newcommand{\isasymreal}{\isamath{\bbbR}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbS}{\isamath{\bbbS}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbT}{\isamath{\bbbT}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbU}{\isamath{\bbbU}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbV}{\isamath{\bbbV}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbW}{\isamath{\bbbW}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbX}{\isamath{\bbbX}}  %requires font txmia from txfonts
+\newcommand{\isasymbbbY}{\isamath{\bbbY}}  %requires font txmia from txfonts
+\newcommand{\isasymint}{\isamath{\bbbZ}}  %requires font txmia from txfonts
 \newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
 \newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
 \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}