--- a/doc-src/AxClass/generated/Group.tex Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex Fri Sep 01 00:27:41 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\isamarkupheader{Basic group theory}
\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}%
@@ -293,7 +294,7 @@
some kind of ``functors'' --- i.e.\ mappings between abstract
theories.%
\end{isamarkuptext}%
-\isacommand{end}\end{isabelle}%
+\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/AxClass/generated/NatClass.tex Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex Fri Sep 01 00:27:41 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
\isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}%
@@ -55,7 +56,7 @@
re-used with some trivial changes only (mostly adding some type
constraints).%
\end{isamarkuptext}%
-\isacommand{end}\end{isabelle}%
+\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/AxClass/generated/Product.tex Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Fri Sep 01 00:27:41 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\isamarkupheader{Syntactic classes}
\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}%
@@ -74,7 +75,7 @@
meta-logic, because there is no internal notion of ``providing
operations'' or even ``names of functions''.%
\end{isamarkuptext}%
-\isacommand{end}\end{isabelle}%
+\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/AxClass/generated/Semigroups.tex Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex Fri Sep 01 00:27:41 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\isamarkupheader{Semigroups}
\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}%
@@ -46,7 +47,7 @@
represent semigroups in a sense, they are certainly not quite the
same.%
\end{isamarkuptext}%
-\isacommand{end}\end{isabelle}%
+\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/AxClass/generated/isabelle.sty Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty Fri Sep 01 00:27:41 2000 +0200
@@ -16,10 +16,14 @@
\newdimen\isa@parindent\newdimen\isa@parskip
-\newenvironment{isabelle}{%
-\trivlist\isa@parindent\parindent\parindent0pt%
+\newenvironment{isabellebody}{%
+\isa@parindent\parindent\parindent0pt%
\isa@parskip\parskip\parskip0pt%
-\isastyle\item\relax}{\endtrivlist}
+\isastyle}{}
+
+\newenvironment{isabelle}
+{\begin{isabellebody}\begin{trivlist}\item\relax}
+{\end{trivlist}\end{isabellebody}}
\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
@@ -62,8 +66,9 @@
% keyword and section markup
+\newcommand{\isakeywordcharunderscore}{\_}
\newcommand{\isakeyword}[1]
-{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}%
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\newcommand{\isacommand}[1]{\isakeyword{#1}}
@@ -90,7 +95,7 @@
\newcommand{\isabellestyleit}{%
\renewcommand{\isastyle}{\small\it}%
\renewcommand{\isastyleminor}{\it}%
-%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
\renewcommand{\isacharbang}{\emph{$!$}}%
\renewcommand{\isachardoublequote}{}%
\renewcommand{\isacharhash}{\emph{$\#$}}%
@@ -111,11 +116,10 @@
\renewcommand{\isacharless}{\emph{$<$}}%
\renewcommand{\isacharequal}{\emph{$=$}}%
\renewcommand{\isachargreater}{\emph{$>$}}%
-%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
\renewcommand{\isacharat}{\emph{$@$}}%
\renewcommand{\isacharbrackleft}{\emph{$[$}}%
\renewcommand{\isacharbrackright}{\emph{$]$}}%
-\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
\renewcommand{\isacharbar}{\emph{$\mid$}}%
\renewcommand{\isacharbraceright}{\emph{$\}$}}%
--- a/doc-src/AxClass/generated/isabellesym.sty Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/isabellesym.sty Fri Sep 01 00:27:41 2000 +0200
@@ -1,15 +1,14 @@
%%
%% $Id$
%%
-%% definitions of many Isabelle symbols
+%% definitions of standard Isabelle symbols
%%
\usepackage{latexsym}
%\usepackage{amssymb}
%\usepackage[latin1]{inputenc}
-\newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack
-%\def\textbrokenbar??? etc
+\newcommand{\bigsqcap}{\overline{|\,\,|}} %an approximation ...
\newcommand{\isasymspacespace}{~~}
\newcommand{\isasymGamma}{$\Gamma$}
@@ -173,15 +172,15 @@
\newcommand{\isasymemptyset}{\emph{$\emptyset$}}
\newcommand{\isasymangle}{\emph{$\angle$}}
\newcommand{\isasymnabla}{\emph{$\nabla$}}
-\newcommand{\isasymProd}{\emph{$\prod$}}
+\newcommand{\isasymProd}{\emph{$\prod\,$}}
\newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}
\newcommand{\isasymUparrow}{\emph{$\Uparrow$}}
\newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}
\newcommand{\isasymlozenge}{\emph{$\lozenge$}}
\newcommand{\isasymlangle}{\emph{$\langle$}}
\newcommand{\isasymrangle}{\emph{$\rangle$}}
-\newcommand{\isasymSum}{\emph{$\sum$}}
-\newcommand{\isasymintegral}{\emph{$\int$}}
+\newcommand{\isasymSum}{\emph{$\sum\,$}}
+\newcommand{\isasymintegral}{\emph{$\int\,$}}
\newcommand{\isasymdagger}{\emph{$\dagger$}}
\newcommand{\isasymsharp}{\emph{$\sharp$}}
\newcommand{\isasymstar}{\emph{$\star$}}
@@ -232,7 +231,7 @@
\newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}
\newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}
-%requires amssymb
+%require amssymb:
\newcommand{\isasymlesssim}{\emph{$\lesssim$}}
\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}
\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}