eliminated copies of isabelle style files;
authorwenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511bf89455ccf9d
parent 42510 b9c106763325
child 42512 f1ca2b0e0265
eliminated copies of isabelle style files;
doc-src/Classes/Makefile
doc-src/Classes/classes.tex
doc-src/Codegen/Makefile
doc-src/Codegen/codegen.tex
doc-src/Functions/Makefile
doc-src/Functions/functions.tex
doc-src/IsarImplementation/Makefile
doc-src/IsarImplementation/implementation.tex
doc-src/IsarOverview/Isar/document/root.tex
doc-src/IsarRef/Makefile
doc-src/IsarRef/isar-ref.tex
doc-src/LaTeXsugar/Makefile
doc-src/LaTeXsugar/Sugar/document/root.tex
doc-src/Locales/Locales/document/root.tex
doc-src/Locales/Makefile
doc-src/Main/Makefile
doc-src/Main/main.tex
doc-src/Nitpick/nitpick.tex
doc-src/Sledgehammer/sledgehammer.tex
doc-src/System/system.tex
doc-src/TutorialI/Makefile
doc-src/TutorialI/tutorial.tex
doc-src/ZF/Makefile
doc-src/ZF/logics-ZF.tex
doc-src/isabelle.sty
doc-src/isabellesym.sty
     1.1 --- a/doc-src/Classes/Makefile	Sun May 01 00:01:59 2011 +0200
     1.2 +++ b/doc-src/Classes/Makefile	Sun May 01 16:36:34 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  FILES = $(NAME).tex classes.tex Thy/document/Classes.tex \
     1.6    style.sty ../iman.sty ../extra.sty ../isar.sty \
     1.7 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
     1.8 +  ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty \
     1.9    ../manual.bib ../proof.sty
    1.10  
    1.11  dvi: $(NAME).dvi
     2.1 --- a/doc-src/Classes/classes.tex	Sun May 01 00:01:59 2011 +0200
     2.2 +++ b/doc-src/Classes/classes.tex	Sun May 01 16:36:34 2011 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  \usepackage{latexsym,graphicx}
     2.5  \usepackage[refpage]{nomencl}
     2.6  \usepackage{../iman,../extra,../isar,../proof}
     2.7 -\usepackage{../isabelle,../isabellesym}
     2.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     2.9  \usepackage{style}
    2.10  \usepackage{../pdfsetup}
    2.11  
     3.1 --- a/doc-src/Codegen/Makefile	Sun May 01 00:01:59 2011 +0200
     3.2 +++ b/doc-src/Codegen/Makefile	Sun May 01 16:36:34 2011 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  FILES = $(NAME).tex Thy/document/*.tex \
     3.6    style.sty ../iman.sty ../extra.sty ../isar.sty \
     3.7 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
     3.8 +  ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty \
     3.9    ../manual.bib ../proof.sty
    3.10  
    3.11  dvi: $(NAME).dvi
     4.1 --- a/doc-src/Codegen/codegen.tex	Sun May 01 00:01:59 2011 +0200
     4.2 +++ b/doc-src/Codegen/codegen.tex	Sun May 01 16:36:34 2011 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  \usepackage[refpage]{nomencl}
     4.5  \usepackage{multirow}
     4.6  \usepackage{../iman,../extra,../isar,../proof}
     4.7 -\usepackage{../isabelle,../isabellesym}
     4.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     4.9  \usepackage{style}
    4.10  \usepackage{../pdfsetup}
    4.11  
     5.1 --- a/doc-src/Functions/Makefile	Sun May 01 00:01:59 2011 +0200
     5.2 +++ b/doc-src/Functions/Makefile	Sun May 01 16:36:34 2011 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  
     5.5  FILES = $(NAME).tex Thy/document/Functions.tex intro.tex conclusion.tex \
     5.6    style.sty ../iman.sty ../extra.sty ../isar.sty \
     5.7 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
     5.8 +  ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty \
     5.9    ../manual.bib ../proof.sty
    5.10  
    5.11  dvi: $(NAME).dvi
     6.1 --- a/doc-src/Functions/functions.tex	Sun May 01 00:01:59 2011 +0200
     6.2 +++ b/doc-src/Functions/functions.tex	Sun May 01 16:36:34 2011 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  \usepackage{latexsym,graphicx}
     6.5  \usepackage[refpage]{nomencl}
     6.6  \usepackage{../iman,../extra,../isar,../proof}
     6.7 -\usepackage{../isabelle,../isabellesym}
     6.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     6.9  \usepackage{style}
    6.10  \usepackage{mathpartir}
    6.11  \usepackage{amsthm}
     7.1 --- a/doc-src/IsarImplementation/Makefile	Sun May 01 00:01:59 2011 +0200
     7.2 +++ b/doc-src/IsarImplementation/Makefile	Sun May 01 16:36:34 2011 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  
     7.5  NAME = implementation
     7.6  
     7.7 -FILES = ../extra.sty ../iman.sty ../isabelle.sty ../isabellesym.sty	\
     7.8 +FILES = ../extra.sty ../iman.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty	\
     7.9    ../isar.sty ../manual.bib ../pdfsetup.sty ../proof.sty ../rail.sty	\
    7.10    ../railsetup.sty Thy/document/Integration.tex Thy/document/Isar.tex	\
    7.11    Thy/document/Local_Theory.tex Thy/document/Logic.tex			\
     8.1 --- a/doc-src/IsarImplementation/implementation.tex	Sun May 01 00:01:59 2011 +0200
     8.2 +++ b/doc-src/IsarImplementation/implementation.tex	Sun May 01 16:36:34 2011 +0200
     8.3 @@ -3,7 +3,7 @@
     8.4  \usepackage[refpage]{nomencl}
     8.5  \usepackage{../iman,../extra,../isar,../proof}
     8.6  \usepackage[nohyphen,strings]{../underscore}
     8.7 -\usepackage{../isabelle,../isabellesym}
     8.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     8.9  \usepackage{../ttbox,../rail,../railsetup}
    8.10  \usepackage{style}
    8.11  \usepackage{../pdfsetup}
     9.1 --- a/doc-src/IsarOverview/Isar/document/root.tex	Sun May 01 00:01:59 2011 +0200
     9.2 +++ b/doc-src/IsarOverview/Isar/document/root.tex	Sun May 01 16:36:34 2011 +0200
     9.3 @@ -1,6 +1,6 @@
     9.4  \documentclass[envcountsame]{llncs}
     9.5  %\documentclass[11pt,a4paper]{article}
     9.6 -\usepackage{../../../isabelle,../../../isabellesym,../../../pdfsetup}
     9.7 +\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym,../../../pdfsetup}
     9.8  
     9.9  %for best-style documents ...
    9.10  \urlstyle{rm}
    10.1 --- a/doc-src/IsarRef/Makefile	Sun May 01 00:01:59 2011 +0200
    10.2 +++ b/doc-src/IsarRef/Makefile	Sun May 01 16:36:34 2011 +0200
    10.3 @@ -17,13 +17,13 @@
    10.4    Thy/document/Introduction.tex Thy/document/Document_Preparation.tex	\
    10.5    Thy/document/Misc.tex Thy/document/Outer_Syntax.tex			\
    10.6    Thy/document/Symbols.tex ../isar.sty ../rail.sty ../railsetup.sty	\
    10.7 -  ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../isabelle.sty	\
    10.8 -  ../isabellesym.sty ../pdfsetup.sty ../manual.bib
    10.9 +  ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../../lib/texinputs/isabelle.sty	\
   10.10 +  ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
   10.11  
   10.12  OUTPUT = syms.tex
   10.13  
   10.14 -syms.tex: showsymbols ../isabellesym.sty
   10.15 -	@./showsymbols <../isabellesym.sty >syms.tex
   10.16 +syms.tex: showsymbols ../../lib/texinputs/isabellesym.sty
   10.17 +	@./showsymbols <../../lib/texinputs/isabellesym.sty >syms.tex
   10.18  
   10.19  
   10.20  dvi: $(NAME).dvi
    11.1 --- a/doc-src/IsarRef/isar-ref.tex	Sun May 01 00:01:59 2011 +0200
    11.2 +++ b/doc-src/IsarRef/isar-ref.tex	Sun May 01 16:36:34 2011 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4  \let\intorig=\int  %iman.sty redefines \int
    11.5  \usepackage{../iman,../extra,../isar,../proof}
    11.6  \usepackage[nohyphen,strings]{../underscore}
    11.7 -\usepackage{../isabelle,../isabellesym}
    11.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    11.9  \usepackage{../ttbox,,../rail,../railsetup}
   11.10  \usepackage{supertabular}
   11.11  \usepackage{style}
    12.1 --- a/doc-src/LaTeXsugar/Makefile	Sun May 01 00:01:59 2011 +0200
    12.2 +++ b/doc-src/LaTeXsugar/Makefile	Sun May 01 16:36:34 2011 +0200
    12.3 @@ -19,7 +19,7 @@
    12.4  FILES = Sugar/document/root.tex Sugar/document/root.bib \
    12.5          Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
    12.6          Sugar/document/OptionalSugar.tex Sugar/document/Sugar.tex \
    12.7 -        ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty
    12.8 +        ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty
    12.9  
   12.10  GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
   12.11            Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \
    13.1 --- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Sun May 01 00:01:59 2011 +0200
    13.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Sun May 01 16:36:34 2011 +0200
    13.3 @@ -1,5 +1,5 @@
    13.4  \documentclass[11pt,a4paper]{article}
    13.5 -\usepackage{../../../isabelle,../../../isabellesym}
    13.6 +\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym}
    13.7  
    13.8  % further packages required for unusual symbols (see also isabellesym.sty)
    13.9  % use only when needed
    14.1 --- a/doc-src/Locales/Locales/document/root.tex	Sun May 01 00:01:59 2011 +0200
    14.2 +++ b/doc-src/Locales/Locales/document/root.tex	Sun May 01 16:36:34 2011 +0200
    14.3 @@ -1,6 +1,6 @@
    14.4  \documentclass[11pt,a4paper]{article}
    14.5  \usepackage{amsmath}
    14.6 -\usepackage{../../../isabelle,../../../isabellesym}
    14.7 +\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym}
    14.8  \usepackage{verbatim}
    14.9  \usepackage{alltt}
   14.10  \usepackage{array}
    15.1 --- a/doc-src/Locales/Makefile	Sun May 01 00:01:59 2011 +0200
    15.2 +++ b/doc-src/Locales/Makefile	Sun May 01 16:36:34 2011 +0200
    15.3 @@ -17,7 +17,7 @@
    15.4    Locales/document/session.tex Locales/document/Examples.tex \
    15.5    Locales/document/Examples1.tex Locales/document/Examples2.tex \
    15.6    Locales/document/Examples3.tex \
    15.7 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty 
    15.8 +  ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty 
    15.9  
   15.10  dvi: $(NAME).dvi
   15.11  
    16.1 --- a/doc-src/Main/Makefile	Sun May 01 00:01:59 2011 +0200
    16.2 +++ b/doc-src/Main/Makefile	Sun May 01 16:36:34 2011 +0200
    16.3 @@ -10,7 +10,7 @@
    16.4  
    16.5  NAME = main
    16.6  
    16.7 -FILES = ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty $(NAME).tex	\
    16.8 +FILES = ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty $(NAME).tex	\
    16.9    Docs/document/Main_Doc.tex
   16.10  
   16.11  dvi: $(NAME).dvi
    17.1 --- a/doc-src/Main/main.tex	Sun May 01 00:01:59 2011 +0200
    17.2 +++ b/doc-src/Main/main.tex	Sun May 01 16:36:34 2011 +0200
    17.3 @@ -8,7 +8,7 @@
    17.4  \headsep=0mm
    17.5  \textheight=234mm
    17.6  
    17.7 -\usepackage{../isabelle,../isabellesym}
    17.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    17.9  \usepackage{amssymb}
   17.10  \usepackage[only,bigsqcap]{stmaryrd}
   17.11  
    18.1 --- a/doc-src/Nitpick/nitpick.tex	Sun May 01 00:01:59 2011 +0200
    18.2 +++ b/doc-src/Nitpick/nitpick.tex	Sun May 01 16:36:34 2011 +0200
    18.3 @@ -10,7 +10,7 @@
    18.4  \usepackage{multicol}
    18.5  \usepackage{stmaryrd}
    18.6  %\usepackage[scaled=.85]{beramono}
    18.7 -\usepackage{../isabelle,../iman,../pdfsetup}
    18.8 +\usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
    18.9  
   18.10  %\oddsidemargin=4.6mm
   18.11  %\evensidemargin=4.6mm
    19.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 00:01:59 2011 +0200
    19.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun May 01 16:36:34 2011 +0200
    19.3 @@ -10,7 +10,7 @@
    19.4  \usepackage{multicol}
    19.5  \usepackage{stmaryrd}
    19.6  %\usepackage[scaled=.85]{beramono}
    19.7 -\usepackage{../isabelle,../iman,../pdfsetup}
    19.8 +\usepackage{../../lib/texinputs/isabelle,../iman,../pdfsetup}
    19.9  
   19.10  %\oddsidemargin=4.6mm
   19.11  %\evensidemargin=4.6mm
    20.1 --- a/doc-src/System/system.tex	Sun May 01 00:01:59 2011 +0200
    20.2 +++ b/doc-src/System/system.tex	Sun May 01 16:36:34 2011 +0200
    20.3 @@ -3,7 +3,7 @@
    20.4  \usepackage{graphicx}
    20.5  \usepackage{../iman,../extra,../isar,../ttbox}
    20.6  \usepackage[nohyphen,strings]{../underscore}
    20.7 -\usepackage{../isabelle,../isabellesym}
    20.8 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    20.9  \usepackage{../IsarRef/style}
   20.10  \usepackage{../pdfsetup}
   20.11  
    21.1 --- a/doc-src/TutorialI/Makefile	Sun May 01 00:01:59 2011 +0200
    21.2 +++ b/doc-src/TutorialI/Makefile	Sun May 01 16:36:34 2011 +0200
    21.3 @@ -24,7 +24,7 @@
    21.4  	Rules/rules.tex Sets/sets.tex Types/numerics.tex		\
    21.5  	Types/types.tex Types/document/Overloading.tex \
    21.6  	Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty	\
    21.7 -	../ttbox.sty ../extra.sty ../isabelle.sty ../isabellesym.sty	\
    21.8 +	../ttbox.sty ../extra.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty	\
    21.9  	../pdfsetup.sty
   21.10  
   21.11  dvi: $(NAME).dvi
    22.1 --- a/doc-src/TutorialI/tutorial.tex	Sun May 01 00:01:59 2011 +0200
    22.2 +++ b/doc-src/TutorialI/tutorial.tex	Sun May 01 16:36:34 2011 +0200
    22.3 @@ -1,6 +1,6 @@
    22.4  \documentclass{article}
    22.5  %%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters
    22.6 -\usepackage{cl2emono-modified,../isabelle,../isabellesym}
    22.7 +\usepackage{cl2emono-modified,../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    22.8  \usepackage{../proof,amsmath,amsfonts}
    22.9  \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
   22.10  \usepackage[greek,english]{babel}
    23.1 --- a/doc-src/ZF/Makefile	Sun May 01 00:01:59 2011 +0200
    23.2 +++ b/doc-src/ZF/Makefile	Sun May 01 16:36:34 2011 +0200
    23.3 @@ -14,7 +14,7 @@
    23.4  NAME = logics-ZF
    23.5  FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty	\
    23.6    ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty	\
    23.7 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty ../manual.bib
    23.8 +  ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
    23.9  
   23.10  dvi: $(NAME).dvi
   23.11  
    24.1 --- a/doc-src/ZF/logics-ZF.tex	Sun May 01 00:01:59 2011 +0200
    24.2 +++ b/doc-src/ZF/logics-ZF.tex	Sun May 01 16:36:34 2011 +0200
    24.3 @@ -1,6 +1,6 @@
    24.4  %% $Id$
    24.5  \documentclass[11pt,a4paper]{report}
    24.6 -\usepackage{../isabelle,../isabellesym}
    24.7 +\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
    24.8  \usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
    24.9  
   24.10  \usepackage{../pdfsetup}   
    25.1 --- a/doc-src/isabelle.sty	Sun May 01 00:01:59 2011 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,218 +0,0 @@
    25.4 -%%
    25.5 -%% macros for Isabelle generated LaTeX output
    25.6 -%%
    25.7 -
    25.8 -%%% Simple document preparation (based on theory token language and symbols)
    25.9 -
   25.10 -% isabelle environments
   25.11 -
   25.12 -\newcommand{\isabellecontext}{UNKNOWN}
   25.13 -
   25.14 -\newcommand{\isastyle}{\UNDEF}
   25.15 -\newcommand{\isastyleminor}{\UNDEF}
   25.16 -\newcommand{\isastylescript}{\UNDEF}
   25.17 -\newcommand{\isastyletext}{\normalsize\rm}
   25.18 -\newcommand{\isastyletxt}{\rm}
   25.19 -\newcommand{\isastylecmt}{\rm}
   25.20 -
   25.21 -%symbol markup -- \emph achieves decent spacing via italic corrections
   25.22 -\newcommand{\isamath}[1]{\emph{$#1$}}
   25.23 -\newcommand{\isatext}[1]{\emph{#1}}
   25.24 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
   25.25 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   25.26 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   25.27 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   25.28 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   25.29 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
   25.30 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
   25.31 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
   25.32 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
   25.33 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
   25.34 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
   25.35 -
   25.36 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
   25.37 -\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
   25.38 -\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
   25.39 -
   25.40 -\newdimen\isa@parindent\newdimen\isa@parskip
   25.41 -
   25.42 -\newenvironment{isabellebody}{%
   25.43 -\isamarkuptrue\par%
   25.44 -\isa@parindent\parindent\parindent0pt%
   25.45 -\isa@parskip\parskip\parskip0pt%
   25.46 -\isastyle}{\par}
   25.47 -
   25.48 -\newenvironment{isabelle}
   25.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
   25.50 -{\end{isabellebody}\end{trivlist}}
   25.51 -
   25.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
   25.53 -
   25.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
   25.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
   25.56 -\newcommand{\isasep}{}
   25.57 -\newcommand{\isadigit}[1]{#1}
   25.58 -
   25.59 -\newcommand{\isachardefaults}{%
   25.60 -\chardef\isacharbang=`\!%
   25.61 -\chardef\isachardoublequote=`\"%
   25.62 -\chardef\isachardoublequoteopen=`\"%
   25.63 -\chardef\isachardoublequoteclose=`\"%
   25.64 -\chardef\isacharhash=`\#%
   25.65 -\chardef\isachardollar=`\$%
   25.66 -\chardef\isacharpercent=`\%%
   25.67 -\chardef\isacharampersand=`\&%
   25.68 -\chardef\isacharprime=`\'%
   25.69 -\chardef\isacharparenleft=`\(%
   25.70 -\chardef\isacharparenright=`\)%
   25.71 -\chardef\isacharasterisk=`\*%
   25.72 -\chardef\isacharplus=`\+%
   25.73 -\chardef\isacharcomma=`\,%
   25.74 -\chardef\isacharminus=`\-%
   25.75 -\chardef\isachardot=`\.%
   25.76 -\chardef\isacharslash=`\/%
   25.77 -\chardef\isacharcolon=`\:%
   25.78 -\chardef\isacharsemicolon=`\;%
   25.79 -\chardef\isacharless=`\<%
   25.80 -\chardef\isacharequal=`\=%
   25.81 -\chardef\isachargreater=`\>%
   25.82 -\chardef\isacharquery=`\?%
   25.83 -\chardef\isacharat=`\@%
   25.84 -\chardef\isacharbrackleft=`\[%
   25.85 -\chardef\isacharbackslash=`\\%
   25.86 -\chardef\isacharbrackright=`\]%
   25.87 -\chardef\isacharcircum=`\^%
   25.88 -\chardef\isacharunderscore=`\_%
   25.89 -\def\isacharunderscorekeyword{\_}%
   25.90 -\chardef\isacharbackquote=`\`%
   25.91 -\chardef\isacharbackquoteopen=`\`%
   25.92 -\chardef\isacharbackquoteclose=`\`%
   25.93 -\chardef\isacharbraceleft=`\{%
   25.94 -\chardef\isacharbar=`\|%
   25.95 -\chardef\isacharbraceright=`\}%
   25.96 -\chardef\isachartilde=`\~%
   25.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
   25.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
   25.99 -}
  25.100 -
  25.101 -\newcommand{\isaliteral}[2]{#2}
  25.102 -\newcommand{\isanil}{}
  25.103 -
  25.104 -
  25.105 -% keyword and section markup
  25.106 -
  25.107 -\newcommand{\isakeyword}[1]
  25.108 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
  25.109 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
  25.110 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
  25.111 -
  25.112 -\newcommand{\isamarkupheader}[1]{\section{#1}}
  25.113 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
  25.114 -\newcommand{\isamarkupsection}[1]{\section{#1}}
  25.115 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
  25.116 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
  25.117 -\newcommand{\isamarkupsect}[1]{\section{#1}}
  25.118 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
  25.119 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
  25.120 -
  25.121 -\newif\ifisamarkup
  25.122 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
  25.123 -\newcommand{\isaendpar}{\par\medskip}
  25.124 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
  25.125 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
  25.126 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
  25.127 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
  25.128 -
  25.129 -
  25.130 -% styles
  25.131 -
  25.132 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
  25.133 -
  25.134 -\newcommand{\isabellestyledefault}{%
  25.135 -\renewcommand{\isastyle}{\small\tt\slshape}%
  25.136 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
  25.137 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
  25.138 -\isachardefaults%
  25.139 -}
  25.140 -\isabellestyledefault
  25.141 -
  25.142 -\newcommand{\isabellestylett}{%
  25.143 -\renewcommand{\isastyle}{\small\tt}%
  25.144 -\renewcommand{\isastyleminor}{\small\tt}%
  25.145 -\renewcommand{\isastylescript}{\footnotesize\tt}%
  25.146 -\isachardefaults%
  25.147 -}
  25.148 -
  25.149 -\newcommand{\isabellestyleit}{%
  25.150 -\renewcommand{\isastyle}{\small\it}%
  25.151 -\renewcommand{\isastyleminor}{\it}%
  25.152 -\renewcommand{\isastylescript}{\footnotesize\it}%
  25.153 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
  25.154 -\renewcommand{\isacharbang}{\isamath{!}}%
  25.155 -\renewcommand{\isachardoublequote}{\isanil}%
  25.156 -\renewcommand{\isachardoublequoteopen}{\isanil}%
  25.157 -\renewcommand{\isachardoublequoteclose}{\isanil}%
  25.158 -\renewcommand{\isacharhash}{\isamath{\#}}%
  25.159 -\renewcommand{\isachardollar}{\isamath{\$}}%
  25.160 -\renewcommand{\isacharpercent}{\isamath{\%}}%
  25.161 -\renewcommand{\isacharampersand}{\isamath{\&}}%
  25.162 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
  25.163 -\renewcommand{\isacharparenleft}{\isamath{(}}%
  25.164 -\renewcommand{\isacharparenright}{\isamath{)}}%
  25.165 -\renewcommand{\isacharasterisk}{\isamath{*}}%
  25.166 -\renewcommand{\isacharplus}{\isamath{+}}%
  25.167 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
  25.168 -\renewcommand{\isacharminus}{\isamath{-}}%
  25.169 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
  25.170 -\renewcommand{\isacharslash}{\isamath{/}}%
  25.171 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
  25.172 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
  25.173 -\renewcommand{\isacharless}{\isamath{<}}%
  25.174 -\renewcommand{\isacharequal}{\isamath{=}}%
  25.175 -\renewcommand{\isachargreater}{\isamath{>}}%
  25.176 -\renewcommand{\isacharat}{\isamath{@}}%
  25.177 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
  25.178 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
  25.179 -\renewcommand{\isacharbrackright}{\isamath{]}}%
  25.180 -\renewcommand{\isacharunderscore}{\mbox{-}}%
  25.181 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
  25.182 -\renewcommand{\isacharbar}{\isamath{\mid}}%
  25.183 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
  25.184 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
  25.185 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
  25.186 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
  25.187 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
  25.188 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
  25.189 -}
  25.190 -
  25.191 -\newcommand{\isabellestylesl}{%
  25.192 -\isabellestyleit%
  25.193 -\renewcommand{\isastyle}{\small\sl}%
  25.194 -\renewcommand{\isastyleminor}{\sl}%
  25.195 -\renewcommand{\isastylescript}{\footnotesize\sl}%
  25.196 -}
  25.197 -
  25.198 -
  25.199 -% tagged regions
  25.200 -
  25.201 -%plain TeX version of comment package -- much faster!
  25.202 -\let\isafmtname\fmtname\def\fmtname{plain}
  25.203 -\usepackage{comment}
  25.204 -\let\fmtname\isafmtname
  25.205 -
  25.206 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
  25.207 -
  25.208 -\newcommand{\isakeeptag}[1]%
  25.209 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
  25.210 -\newcommand{\isadroptag}[1]%
  25.211 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
  25.212 -\newcommand{\isafoldtag}[1]%
  25.213 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
  25.214 -
  25.215 -\isakeeptag{theory}
  25.216 -\isakeeptag{proof}
  25.217 -\isakeeptag{ML}
  25.218 -\isakeeptag{visible}
  25.219 -\isadroptag{invisible}
  25.220 -
  25.221 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
    26.1 --- a/doc-src/isabellesym.sty	Sun May 01 00:01:59 2011 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,360 +0,0 @@
    26.4 -%%
    26.5 -%% definitions of standard Isabelle symbols
    26.6 -%%
    26.7 -
    26.8 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
    26.9 -\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb
   26.10 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb
   26.11 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb
   26.12 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
   26.13 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
   26.14 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb
   26.15 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb
   26.16 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb
   26.17 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
   26.18 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
   26.19 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
   26.20 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
   26.21 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
   26.22 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
   26.23 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
   26.24 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
   26.25 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
   26.26 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
   26.27 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
   26.28 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
   26.29 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
   26.30 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
   26.31 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
   26.32 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
   26.33 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
   26.34 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
   26.35 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
   26.36 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
   26.37 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
   26.38 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
   26.39 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
   26.40 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
   26.41 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
   26.42 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
   26.43 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
   26.44 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
   26.45 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
   26.46 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
   26.47 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
   26.48 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
   26.49 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
   26.50 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
   26.51 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
   26.52 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
   26.53 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
   26.54 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
   26.55 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
   26.56 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
   26.57 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
   26.58 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
   26.59 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
   26.60 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
   26.61 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
   26.62 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
   26.63 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
   26.64 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
   26.65 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
   26.66 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
   26.67 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
   26.68 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
   26.69 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
   26.70 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
   26.71 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
   26.72 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
   26.73 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
   26.74 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
   26.75 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
   26.76 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
   26.77 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
   26.78 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
   26.79 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
   26.80 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
   26.81 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
   26.82 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
   26.83 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
   26.84 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
   26.85 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
   26.86 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
   26.87 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
   26.88 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
   26.89 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
   26.90 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
   26.91 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
   26.92 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
   26.93 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
   26.94 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
   26.95 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
   26.96 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
   26.97 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
   26.98 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
   26.99 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
  26.100 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
  26.101 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
  26.102 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
  26.103 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
  26.104 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
  26.105 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
  26.106 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
  26.107 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
  26.108 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
  26.109 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
  26.110 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
  26.111 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
  26.112 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
  26.113 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
  26.114 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
  26.115 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
  26.116 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
  26.117 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
  26.118 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
  26.119 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
  26.120 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
  26.121 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
  26.122 -\newcommand{\isasymalpha}{\isamath{\alpha}}
  26.123 -\newcommand{\isasymbeta}{\isamath{\beta}}
  26.124 -\newcommand{\isasymgamma}{\isamath{\gamma}}
  26.125 -\newcommand{\isasymdelta}{\isamath{\delta}}
  26.126 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
  26.127 -\newcommand{\isasymzeta}{\isamath{\zeta}}
  26.128 -\newcommand{\isasymeta}{\isamath{\eta}}
  26.129 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
  26.130 -\newcommand{\isasymiota}{\isamath{\iota}}
  26.131 -\newcommand{\isasymkappa}{\isamath{\kappa}}
  26.132 -\newcommand{\isasymlambda}{\isamath{\lambda}}
  26.133 -\newcommand{\isasymmu}{\isamath{\mu}}
  26.134 -\newcommand{\isasymnu}{\isamath{\nu}}
  26.135 -\newcommand{\isasymxi}{\isamath{\xi}}
  26.136 -\newcommand{\isasympi}{\isamath{\pi}}
  26.137 -\newcommand{\isasymrho}{\isamath{\varrho}}
  26.138 -\newcommand{\isasymsigma}{\isamath{\sigma}}
  26.139 -\newcommand{\isasymtau}{\isamath{\tau}}
  26.140 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
  26.141 -\newcommand{\isasymphi}{\isamath{\varphi}}
  26.142 -\newcommand{\isasymchi}{\isamath{\chi}}
  26.143 -\newcommand{\isasympsi}{\isamath{\psi}}
  26.144 -\newcommand{\isasymomega}{\isamath{\omega}}
  26.145 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
  26.146 -\newcommand{\isasymDelta}{\isamath{\Delta}}
  26.147 -\newcommand{\isasymTheta}{\isamath{\Theta}}
  26.148 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
  26.149 -\newcommand{\isasymXi}{\isamath{\Xi}}
  26.150 -\newcommand{\isasymPi}{\isamath{\Pi}}
  26.151 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
  26.152 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
  26.153 -\newcommand{\isasymPhi}{\isamath{\Phi}}
  26.154 -\newcommand{\isasymPsi}{\isamath{\Psi}}
  26.155 -\newcommand{\isasymOmega}{\isamath{\Omega}}
  26.156 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
  26.157 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
  26.158 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
  26.159 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
  26.160 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
  26.161 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
  26.162 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
  26.163 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
  26.164 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
  26.165 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
  26.166 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
  26.167 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
  26.168 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
  26.169 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
  26.170 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
  26.171 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
  26.172 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
  26.173 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
  26.174 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
  26.175 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
  26.176 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
  26.177 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
  26.178 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
  26.179 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
  26.180 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
  26.181 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
  26.182 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
  26.183 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
  26.184 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
  26.185 -\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
  26.186 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
  26.187 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
  26.188 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
  26.189 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
  26.190 -\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
  26.191 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
  26.192 -\newcommand{\isasymup}{\isamath{\uparrow}}
  26.193 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
  26.194 -\newcommand{\isasymdown}{\isamath{\downarrow}}
  26.195 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
  26.196 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
  26.197 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
  26.198 -\newcommand{\isasymlangle}{\isamath{\langle}}
  26.199 -\newcommand{\isasymrangle}{\isamath{\rangle}}
  26.200 -\newcommand{\isasymlceil}{\isamath{\lceil}}
  26.201 -\newcommand{\isasymrceil}{\isamath{\rceil}}
  26.202 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
  26.203 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
  26.204 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
  26.205 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
  26.206 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
  26.207 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
  26.208 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
  26.209 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
  26.210 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
  26.211 -\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
  26.212 -\newcommand{\isasymbottom}{\isamath{\bot}}
  26.213 -\newcommand{\isasymtop}{\isamath{\top}}
  26.214 -\newcommand{\isasymand}{\isamath{\wedge}}
  26.215 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
  26.216 -\newcommand{\isasymor}{\isamath{\vee}}
  26.217 -\newcommand{\isasymOr}{\isamath{\bigvee}}
  26.218 -\newcommand{\isasymforall}{\isamath{\forall\,}}
  26.219 -\newcommand{\isasymexists}{\isamath{\exists\,}}
  26.220 -\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
  26.221 -\newcommand{\isasymnot}{\isamath{\neg}}
  26.222 -\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
  26.223 -\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
  26.224 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
  26.225 -\newcommand{\isasymTurnstile}{\isamath{\models}}
  26.226 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
  26.227 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
  26.228 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
  26.229 -\newcommand{\isasymsurd}{\isamath{\surd}}
  26.230 -\newcommand{\isasymle}{\isamath{\le}}
  26.231 -\newcommand{\isasymge}{\isamath{\ge}}
  26.232 -\newcommand{\isasymlless}{\isamath{\ll}}
  26.233 -\newcommand{\isasymggreater}{\isamath{\gg}}
  26.234 -\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
  26.235 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
  26.236 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
  26.237 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
  26.238 -\newcommand{\isasymin}{\isamath{\in}}
  26.239 -\newcommand{\isasymnotin}{\isamath{\notin}}
  26.240 -\newcommand{\isasymsubset}{\isamath{\subset}}
  26.241 -\newcommand{\isasymsupset}{\isamath{\supset}}
  26.242 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
  26.243 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
  26.244 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
  26.245 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
  26.246 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
  26.247 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
  26.248 -\newcommand{\isasyminter}{\isamath{\cap}}
  26.249 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
  26.250 -\newcommand{\isasymunion}{\isamath{\cup}}
  26.251 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
  26.252 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
  26.253 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
  26.254 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
  26.255 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
  26.256 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
  26.257 -\newcommand{\isasympropto}{\isamath{\propto}}
  26.258 -\newcommand{\isasymuplus}{\isamath{\uplus}}
  26.259 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
  26.260 -\newcommand{\isasymnoteq}{\isamath{\not=}}
  26.261 -\newcommand{\isasymsim}{\isamath{\sim}}
  26.262 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
  26.263 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
  26.264 -\newcommand{\isasymapprox}{\isamath{\approx}}
  26.265 -\newcommand{\isasymasymp}{\isamath{\asymp}}
  26.266 -\newcommand{\isasymcong}{\isamath{\cong}}
  26.267 -\newcommand{\isasymsmile}{\isamath{\smile}}
  26.268 -\newcommand{\isasymequiv}{\isamath{\equiv}}
  26.269 -\newcommand{\isasymfrown}{\isamath{\frown}}
  26.270 -\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
  26.271 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
  26.272 -\newcommand{\isasymprec}{\isamath{\prec}}
  26.273 -\newcommand{\isasymsucc}{\isamath{\succ}}
  26.274 -\newcommand{\isasympreceq}{\isamath{\preceq}}
  26.275 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
  26.276 -\newcommand{\isasymparallel}{\isamath{\parallel}}
  26.277 -\newcommand{\isasymbar}{\isamath{\mid}}
  26.278 -\newcommand{\isasymplusminus}{\isamath{\pm}}
  26.279 -\newcommand{\isasymminusplus}{\isamath{\mp}}
  26.280 -\newcommand{\isasymtimes}{\isamath{\times}}
  26.281 -\newcommand{\isasymdiv}{\isamath{\div}}
  26.282 -\newcommand{\isasymcdot}{\isamath{\cdot}}
  26.283 -\newcommand{\isasymstar}{\isamath{\star}}
  26.284 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
  26.285 -\newcommand{\isasymcirc}{\isamath{\circ}}
  26.286 -\newcommand{\isasymdagger}{\isamath{\dagger}}
  26.287 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
  26.288 -\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
  26.289 -\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
  26.290 -\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
  26.291 -\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
  26.292 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
  26.293 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
  26.294 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
  26.295 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
  26.296 -\newcommand{\isasymoplus}{\isamath{\oplus}}
  26.297 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
  26.298 -\newcommand{\isasymotimes}{\isamath{\otimes}}
  26.299 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
  26.300 -\newcommand{\isasymodot}{\isamath{\odot}}
  26.301 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
  26.302 -\newcommand{\isasymominus}{\isamath{\ominus}}
  26.303 -\newcommand{\isasymoslash}{\isamath{\oslash}}
  26.304 -\newcommand{\isasymdots}{\isamath{\dots}}
  26.305 -\newcommand{\isasymcdots}{\isamath{\cdots}}
  26.306 -\newcommand{\isasymSum}{\isamath{\sum\,}}
  26.307 -\newcommand{\isasymProd}{\isamath{\prod\,}}
  26.308 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
  26.309 -\newcommand{\isasyminfinity}{\isamath{\infty}}
  26.310 -\newcommand{\isasymintegral}{\isamath{\int\,}}
  26.311 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
  26.312 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
  26.313 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
  26.314 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
  26.315 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
  26.316 -\newcommand{\isasymaleph}{\isamath{\aleph}}
  26.317 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
  26.318 -\newcommand{\isasymnabla}{\isamath{\nabla}}
  26.319 -\newcommand{\isasympartial}{\isamath{\partial}}
  26.320 -\newcommand{\isasymRe}{\isamath{\Re}}
  26.321 -\newcommand{\isasymIm}{\isamath{\Im}}
  26.322 -\newcommand{\isasymflat}{\isamath{\flat}}
  26.323 -\newcommand{\isasymnatural}{\isamath{\natural}}
  26.324 -\newcommand{\isasymsharp}{\isamath{\sharp}}
  26.325 -\newcommand{\isasymangle}{\isamath{\angle}}
  26.326 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
  26.327 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
  26.328 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
  26.329 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
  26.330 -\newcommand{\isasymonesuperior}{\isamath{{}^1}}
  26.331 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires textcomp
  26.332 -\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
  26.333 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires textcomp
  26.334 -\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
  26.335 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires textcomp
  26.336 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
  26.337 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
  26.338 -\newcommand{\isasymsection}{\isatext{\rm\S}}
  26.339 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
  26.340 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
  26.341 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
  26.342 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
  26.343 -\newcommand{\isasympounds}{\isamath{\pounds}}
  26.344 -\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
  26.345 -\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
  26.346 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
  26.347 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires textcomp
  26.348 -\newcommand{\isasymamalg}{\isamath{\amalg}}
  26.349 -\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
  26.350 -\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
  26.351 -\newcommand{\isasymwp}{\isamath{\wp}}
  26.352 -\newcommand{\isasymwrong}{\isamath{\wr}}
  26.353 -\newcommand{\isasymstruct}{\isamath{\diamond}}
  26.354 -\newcommand{\isasymacute}{\isatext{\'\relax}}
  26.355 -\newcommand{\isasymindex}{\isatext{\i}}
  26.356 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
  26.357 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
  26.358 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
  26.359 -\newcommand{\isasymspacespace}{\isamath{~~}}
  26.360 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
  26.361 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
  26.362 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
  26.363 -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}