--- 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
--- 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,
--- 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
--- 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
--- 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,
--- 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
--- 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}%
}
--- 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
--- 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\)
--- 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}
--- 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}
--- 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 \\