# HG changeset patch
# User wenzelm
# Date 971632316 -7200
# Node ID 31346d22bb543882a8bd4bc12994c3c0ebb424c4
# Parent  027a6f43e4080a1cda1361bc1702c3fa834bc23d
tuned;

diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Sun Oct 15 19:51:56 2000 +0200
@@ -200,8 +200,8 @@
 qed
 
 text {*
- \medskip The $\isakeyword{instance}$ command sets up an appropriate
- goal that represents the class inclusion (or type arity, see
+ \medskip The $\INSTANCE$ command sets up an appropriate goal that
+ represents the class inclusion (or type arity, see
  \secref{sec:inst-arity}) to be proven (see also
  \cite{isabelle-isar-ref}).  The @{text intro_classes} proof method
  does back-chaining of class membership statements wrt.\ the hierarchy
@@ -215,14 +215,15 @@
 subsection {* Concrete instantiation \label{sec:inst-arity} *}
 
 text {*
- So far we have covered the case of the form
- $\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
- instantiation} --- $c@1$ is more special than $c@2$ and thus an
- instance of $c@2$.  Even more interesting for practical applications
- are \emph{concrete instantiations} of axiomatic type classes.  That
- is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
- class membership may be established at the logical level and then
- transferred to Isabelle's type signature level.
+ So far we have covered the case of the form $\INSTANCE$~@{text
+ "c\<^sub>1 < c\<^sub>2"}, namely \emph{abstract instantiation} ---
+ $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
+ of @{text "c\<^sub>2"}.  Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes.  That is, certain simple schemes
+ @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be
+ established at the logical level and then transferred to Isabelle's
+ type signature level.
 
  \medskip As a typical example, we show that type @{typ bool} with
  exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
@@ -260,10 +261,10 @@
 qed
 
 text {*
- The result of an $\isakeyword{instance}$ statement is both expressed
- as a theorem of Isabelle's meta-logic, and as a type arity of the
- type signature.  The latter enables type-inference system to take
- care of this new instance automatically.
+ The result of an $\INSTANCE$ statement is both expressed as a theorem
+ of Isabelle's meta-logic, and as a type arity of the type signature.
+ The latter enables type-inference system to take care of this new
+ instance automatically.
 
  \medskip We could now also instantiate our group theory classes to
  many other concrete types.  For example, @{text "int \<Colon> agroup"}
@@ -281,9 +282,9 @@
 text {*
  As already mentioned above, overloading in the simply-typed HOL
  systems may include recursion over the syntactic structure of types.
- That is, definitional equations $c^\tau \equiv t$ may also contain
- constants of name $c$ on the right-hand side --- if these have types
- that are structurally simpler than $\tau$.
+ That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
+ contain constants of name @{text c} on the right-hand side --- if
+ these have types that are structurally simpler than @{text \<tau>}.
 
  This feature enables us to \emph{lift operations}, say to Cartesian
  products, direct sums or function spaces.  Subsequently we lift
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Sun Oct 15 19:51:56 2000 +0200
@@ -41,8 +41,8 @@
  Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
  type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
  type signature.  In our example, this arity may be always added when
- required by means of an $\isarkeyword{instance}$ with the trivial
- proof $\BY{intro_classes}$.
+ required by means of an $\INSTANCE$ with the trivial proof
+ $\BY{intro_classes}$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
@@ -65,11 +65,11 @@
  known to the type checker.
 
  \medskip It is very important to see that above $\DEFS$ are not
- directly connected with $\isarkeyword{instance}$ at all!  We were
- just following our convention to specify @{text \<odot>} on @{typ bool}
- after having instantiated @{text "bool \<Colon> product"}.  Isabelle does
- not require these definitions, which is in contrast to programming
- languages like Haskell \cite{haskell-report}.
+ directly connected with $\INSTANCE$ at all!  We were just following
+ our convention to specify @{text \<odot>} on @{typ bool} after having
+ instantiated @{text "bool \<Colon> product"}.  Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy	Sun Oct 15 19:51:56 2000 +0200
@@ -34,9 +34,9 @@
  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier @{typ 'a} and a fixed
  \emph{signature}.  Different signatures require different classes.
- Below, class @{text plus_semigroup} represents semigroups of the form
- @{text "(\<tau>, \<oplus>)"}, while the original @{text semigroup} would
- correspond to semigroups @{text "(\<tau>, \<odot>)"}.
+ Below, class @{text plus_semigroup} represents semigroups 
+ @{text "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
+ correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
 *}
 
 consts
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -180,8 +180,8 @@
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
-\medskip The $\isakeyword{instance}$ command sets up an appropriate
- goal that represents the class inclusion (or type arity, see
+\medskip The $\INSTANCE$ command sets up an appropriate goal that
+ represents the class inclusion (or type arity, see
  \secref{sec:inst-arity}) to be proven (see also
  \cite{isabelle-isar-ref}).  The \isa{intro{\isacharunderscore}classes} proof method
  does back-chaining of class membership statements wrt.\ the hierarchy
@@ -194,14 +194,14 @@
 \isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
 %
 \begin{isamarkuptext}%
-So far we have covered the case of the form
- $\isakeyword{instance}~c@1 < c@2$, namely \emph{abstract
- instantiation} --- $c@1$ is more special than $c@2$ and thus an
- instance of $c@2$.  Even more interesting for practical applications
- are \emph{concrete instantiations} of axiomatic type classes.  That
- is, certain simple schemes $(\alpha@1, \ldots, \alpha@n)t :: c$ of
- class membership may be established at the logical level and then
- transferred to Isabelle's type signature level.
+So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isacharless}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
+ $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
+ of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes.  That is, certain simple schemes
+ \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be
+ established at the logical level and then transferred to Isabelle's
+ type signature level.
 
  \medskip As a typical example, we show that type \isa{bool} with
  exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
@@ -235,10 +235,10 @@
 \ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
-The result of an $\isakeyword{instance}$ statement is both expressed
- as a theorem of Isabelle's meta-logic, and as a type arity of the
- type signature.  The latter enables type-inference system to take
- care of this new instance automatically.
+The result of an $\INSTANCE$ statement is both expressed as a theorem
+ of Isabelle's meta-logic, and as a type arity of the type signature.
+ The latter enables type-inference system to take care of this new
+ instance automatically.
 
  \medskip We could now also instantiate our group theory classes to
  many other concrete types.  For example, \isa{int\ {\isasymColon}\ agroup}
@@ -255,9 +255,9 @@
 \begin{isamarkuptext}%
 As already mentioned above, overloading in the simply-typed HOL
  systems may include recursion over the syntactic structure of types.
- That is, definitional equations $c^\tau \equiv t$ may also contain
- constants of name $c$ on the right-hand side --- if these have types
- that are structurally simpler than $\tau$.
+ That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
+ contain constants of name \isa{c} on the right-hand side --- if
+ these have types that are structurally simpler than \isa{{\isasymtau}}.
 
  This feature enables us to \emph{lift operations}, say to Cartesian
  products, direct sums or function spaces.  Subsequently we lift
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -40,8 +40,8 @@
  Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
  type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
  type signature.  In our example, this arity may be always added when
- required by means of an $\isarkeyword{instance}$ with the trivial
- proof $\BY{intro_classes}$.
+ required by means of an $\INSTANCE$ with the trivial proof
+ $\BY{intro_classes}$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
@@ -62,11 +62,11 @@
  known to the type checker.
 
  \medskip It is very important to see that above $\DEFS$ are not
- directly connected with $\isarkeyword{instance}$ at all!  We were
- just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
- after having instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does
- not require these definitions, which is in contrast to programming
- languages like Haskell \cite{haskell-report}.
+ directly connected with $\INSTANCE$ at all!  We were just following
+ our convention to specify \isa{{\isasymodot}} on \isa{bool} after having
+ instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does not require
+ these definitions, which is in contrast to programming languages like
+ Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -31,9 +31,9 @@
  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
  \emph{signature}.  Different signatures require different classes.
- Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups of the form
- \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}{\isacharparenright}}, while the original \isa{semigroup} would
- correspond to semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}{\isacharparenright}}.%
+ Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups 
+ \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
+ correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/generated/isabelle.sty
--- a/doc-src/AxClass/generated/isabelle.sty	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty	Sun Oct 15 19:51:56 2000 +0200
@@ -14,10 +14,18 @@
 
 \newcommand{\isastyle}{\small\tt\slshape}
 \newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
 \newcommand{\isastyletext}{\normalsize\rm}
 \newcommand{\isastyletxt}{\rm}
 \newcommand{\isastylecmt}{\rm}
 
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}_{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}^{#1}$}}
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -99,43 +107,46 @@
 \newcommand{\isabellestylett}{%
 \renewcommand{\isastyle}{\small\tt}%
 \renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
 }
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
 \renewcommand{\isachardoublequote}{}%
-\renewcommand{\isacharhash}{\emph{$\#$}}%
-\renewcommand{\isachardollar}{\emph{$\$$}}%
-\renewcommand{\isacharpercent}{\emph{$\%$}}%
-\renewcommand{\isacharampersand}{\emph{$\&$}}%
-\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
-\renewcommand{\isacharparenleft}{\emph{$($}}%
-\renewcommand{\isacharparenright}{\emph{$)$}}%
-\renewcommand{\isacharasterisk}{\emph{$*$}}%
-\renewcommand{\isacharplus}{\emph{$+$}}%
-\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
-\renewcommand{\isacharminus}{\emph{$-$}}%
-\renewcommand{\isachardot}{\emph{$\mathord.$}}%
-\renewcommand{\isacharslash}{\emph{$/$}}%
-\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
-\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
-\renewcommand{\isacharless}{\emph{$<$}}%
-\renewcommand{\isacharequal}{\emph{$=$}}%
-\renewcommand{\isachargreater}{\emph{$>$}}%
-\renewcommand{\isacharat}{\emph{$@$}}%
-\renewcommand{\isacharbrackleft}{\emph{$[$}}%
-\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
 \renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
-\renewcommand{\isacharbar}{\emph{$\mid$}}%
-\renewcommand{\isacharbraceright}{\emph{$\}$}}%
-\renewcommand{\isachartilde}{\emph{${}^\sim$}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}^\sim}}%
 }
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \renewcommand{\isastyle}{\small\sl}%
 \renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
 }
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/AxClass/generated/isabellesym.sty
--- a/doc-src/AxClass/generated/isabellesym.sty	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/AxClass/generated/isabellesym.sty	Sun Oct 15 19:51:56 2000 +0200
@@ -14,13 +14,6 @@
 %\usepackage[only,bigsqcap]{stmaryrd}
 %\usepackage{wasysym}
 
-% Note: \emph is important for proper spacing in fake math mode, it
-% automatically inserts italic corrections around symbols wherever
-% appropriate.
-
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-
 
 % symbol definitions
 
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/IsarRef/conversion.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -165,9 +165,9 @@
 This form may be turned into an Isar tactic-emulation script like this:
 \begin{matharray}{l}
   \LEMMA{name}\texttt"{\phi}\texttt" \\
-  \quad \isarkeyword{apply}~meth@1 \\
+  \quad \APPLY{meth@1} \\
   \qquad \vdots \\
-  \quad \isarkeyword{done} \\
+  \quad \DONE \\
 \end{matharray}
 Note that the main statement may be $\THEOREMNAME$ as well.  See
 \S\ref{sec:conv-tac} for further details on how to convert actual tactic
@@ -183,7 +183,7 @@
 This is replaced by using the $unfold$ proof method explicitly.
 \begin{matharray}{l}
 \LEMMA{name}\texttt"{\phi}\texttt" \\
-\quad \isarkeyword{apply}~(unfold~def@1~\dots) \\
+\quad \APPLY{unfold~def@1~\dots} \\
 \end{matharray}
 
 %FIXME "goal" and higher-order rules;
@@ -192,11 +192,10 @@
 \subsection{Tactics}\label{sec:conv-tac}
 
 Isar Proof methods closely resemble traditional tactics, when used in
-unstructured sequences of $\isarkeyword{apply}$ commands (cf.\ 
-\S\ref{sec:conv-goal}).  Isabelle/Isar provides emulations for all major ML
-tactics of classic Isabelle --- mostly for the sake of easy porting of
-existing developments, as actual Isar proof texts would demand much less
-diversity of proof methods.
+unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
+Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle
+--- mostly for the sake of easy porting of existing developments, as actual
+Isar proof texts would demand much less diversity of proof methods.
 
 Unlike tactic expressions in ML, Isar proof methods provide proper concrete
 syntax for additional arguments, options, modifiers etc.  Thus a typical
@@ -385,25 +384,25 @@
 The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
 replaced by passing the result of a proof through $rule_format$.
 
-\medskip Global ML declarations may be expressed using the
-$\isarkeyword{declare}$ command (see \S\ref{sec:tactic-commands}) together
-with appropriate attributes.  The most common ones are as follows.
+\medskip Global ML declarations may be expressed using the $\DECLARE$ command
+(see \S\ref{sec:tactic-commands}) together with appropriate attributes.  The
+most common ones are as follows.
 \begin{matharray}{lll}
-  \texttt{Addsimps}~[thm] & & \isarkeyword{declare}~thm~[simp] \\
-  \texttt{Delsimps}~[thm] & & \isarkeyword{declare}~thm~[simp~del] \\
-  \texttt{Addsplits}~[thm] & & \isarkeyword{declare}~thm~[split] \\
-  \texttt{Delsplits}~[thm] & & \isarkeyword{declare}~thm~[split~del] \\[0.5ex]
-  \texttt{AddIs}~[thm] & & \isarkeyword{declare}~thm~[intro] \\
-  \texttt{AddEs}~[thm] & & \isarkeyword{declare}~thm~[elim] \\
-  \texttt{AddDs}~[thm] & & \isarkeyword{declare}~thm~[dest] \\
-  \texttt{AddSIs}~[thm] & & \isarkeyword{declare}~thm~[intro!] \\
-  \texttt{AddSEs}~[thm] & & \isarkeyword{declare}~thm~[elim!] \\
-  \texttt{AddSDs}~[thm] & & \isarkeyword{declare}~thm~[dest!] \\[0.5ex]
-  \texttt{AddIffs}~[thm] & & \isarkeyword{declare}~thm~[iff] \\
+  \texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\
+  \texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\
+  \texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\
+  \texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]
+  \texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\
+  \texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\
+  \texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\
+  \texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\
+  \texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\
+  \texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]
+  \texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\
 \end{matharray}
-Note that explicit $\isarkeyword{declare}$ commands are actually needed only
-very rarely; Isar admits to declare theorems on-the-fly wherever they emerge.
-Consider the following ML idiom:
+Note that explicit $\DECLARE$ commands are actually needed only very rarely;
+Isar admits to declare theorems on-the-fly wherever they emerge.  Consider the
+following ML idiom:
 \begin{ttbox}
 Goal "\(\phi\)";
  \(\vdots\)
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -30,20 +30,18 @@
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
-  class as the intersection of existing classes, with additional axioms
-  holding.  Class axioms may not contain more than one type variable.  The
-  class axioms (with implicit sort constraints added) are bound to the given
-  names.  Furthermore a class introduction rule is generated, which is
-  employed by method $intro_classes$ to support instantiation proofs of this
-  class.
-
-\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
-  (\vec s)c$] setup a goal stating a class relation or type arity.  The proof
-  would usually proceed by $intro_classes$, and then establish the
-  characteristic theorems of the type classes involved.  After finishing the
-  proof, the theory will be augmented by a type signature declaration
-  corresponding to the resulting theorem.
+\item [$\AXCLASS~c < \vec c~axms$] defines an axiomatic type class as the
+  intersection of existing classes, with additional axioms holding.  Class
+  axioms may not contain more than one type variable.  The class axioms (with
+  implicit sort constraints added) are bound to the given names.  Furthermore
+  a class introduction rule is generated, which is employed by method
+  $intro_classes$ to support instantiation proofs of this class.
+  
+\item [$\INSTANCE~c@1 < c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a goal
+  stating a class relation or type arity.  The proof would usually proceed by
+  $intro_classes$, and then establish the characteristic theorems of the type
+  classes involved.  After finishing the proof, the theory will be augmented
+  by a type signature declaration corresponding to the resulting theorem.
 \item [$intro_classes$] repeatedly expands all class introduction rules of
   this theory.
 \end{descr}
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -170,8 +170,8 @@
   of existing classes $\vec c$.  Cyclic class structures are ruled out.
 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
   existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
-  $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
-  introduce proven class relations.
+  $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
+  proven class relations.
 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
   any type variables given without sort constraints.  Usually, the default
   sort would be only changed when defining new object-logics.
@@ -213,8 +213,8 @@
   Isabelle's inner syntax of terms or types.
 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
   signature of types by new type constructor arities.  This is done
-  axiomatically!  The $\isarkeyword{instance}$ command (see
-  \S\ref{sec:axclass}) provides a way to introduce proven type arities.
+  axiomatically!  The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
+  way to introduce proven type arities.
 \end{descr}
 
 
@@ -1083,13 +1083,13 @@
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in initial
-  position, but unlike $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus
-  consecutive method applications may be given just as in tactic scripts.
+\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
+  $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus consecutive method
+  applications may be given just as in tactic scripts.
   
   Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
-  are \emph{consumed} afterwards.  Thus any further $\isarkeyword{apply}$
-  command would always work in a purely backward manner.
+  are \emph{consumed} afterwards.  Thus any further $\APPLYNAME$ command would
+  always work in a purely backward manner.
   
 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
   terminal position.  Basically, this simulates a multi-step tactic script for
@@ -1121,9 +1121,8 @@
 \end{descr}
 
 Any proper Isar proof method may be used with tactic script commands such as
-$\isarkeyword{apply}$.  A few additional emulations of actual tactics are
-provided as well; these would be never used in actual structured proofs, of
-course.
+$\APPLYNAME$.  A few additional emulations of actual tactics are provided as
+well; these would be never used in actual structured proofs, of course.
 
 
 \subsection{Meta-linguistic features}
diff -r 027a6f43e408 -r 31346d22bb54 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Sun Oct 15 19:51:19 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Sun Oct 15 19:51:56 2000 +0200
@@ -136,7 +136,7 @@
 \subsection{Commands}
 
 \begin{tabular}{ll}
-  $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\
+  $\APPLY{m}$ & apply proof method at initial position \\
   $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
   $\isarkeyword{done}$ & complete proof \\
   $\isarkeyword{defer}~n$ & move subgoal to end \\