summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 15 Oct 2000 19:51:56 +0200 | |

changeset 10223 | 31346d22bb54 |

parent 10222 | 027a6f43e408 |

child 10224 | 7263c856787e |

tuned;

--- 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 \\