# HG changeset patch
# User wenzelm
# Date 967760861 -7200
# Node ID dc2ee9b2e065427649ef1452f64f4ed6bbdc8df9
# Parent  da6788606f54eb9cf976c61e489e3ebd1317e327
updated;

diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/Group.tex
--- 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"
diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/NatClass.tex
--- 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"
diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/Product.tex
--- 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"
diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/Semigroups.tex
--- 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"
diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/isabelle.sty
--- 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{$\}$}}%
diff -r da6788606f54 -r dc2ee9b2e065 doc-src/AxClass/generated/isabellesym.sty
--- 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$}}