# HG changeset patch
# User wenzelm
# Date 1001622597 -7200
# Node ID 99103cef5f29d20e13850ecf64eb8519705d111c
# Parent  3f3d1add4d94bbf532a19a3cb7deedffe4ee1eec
updated;

diff -r 3f3d1add4d94 -r 99103cef5f29 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Thu Sep 27 22:28:16 2001 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Thu Sep 27 22:29:57 2001 +0200
@@ -24,6 +24,7 @@
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
 
diff -r 3f3d1add4d94 -r 99103cef5f29 doc-src/TutorialI/isabellesym.sty
--- a/doc-src/TutorialI/isabellesym.sty	Thu Sep 27 22:28:16 2001 +0200
+++ b/doc-src/TutorialI/isabellesym.sty	Thu Sep 27 22:29:57 2001 +0200
@@ -5,16 +5,6 @@
 %% definitions of standard Isabelle symbols
 %%
 
-% Required packages for unusual symbols -- see below for details.
-%\usepackage{latexsym}
-%\usepackage{amssymb}
-%\usepackage[english]{babel}
-%\usepackage[latin1]{inputenc}
-%\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{wasysym}
-%\usepackage{eufrak}
-
-
 % symbol definitions
 
 \newcommand{\isasymA}{\isamath{\mathcal{A}}}
@@ -273,10 +263,10 @@
 \newcommand{\isasymdiv}{\isamath{\div}}
 \newcommand{\isasymcdot}{\isamath{\cdot}}
 \newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
 \newcommand{\isasymdagger}{\isamath{\dagger}}
 \newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymcirc}{\isamath{\circ}}
-\newcommand{\isasymbullet}{\isamath{\bullet}}
 \newcommand{\isasymlhd}{\isamath{\lhd}}
 \newcommand{\isasymrhd}{\isamath{\rhd}}
 \newcommand{\isasymunlhd}{\isamath{\unlhd}}