--- a/doc-src/IsarRef/Thy/document/Framework.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Sun Feb 15 18:56:13 2009 +0100
@@ -1511,7 +1511,6 @@
\isadelimtheory
%
\endisadelimtheory
-\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 15 18:56:13 2009 +0100
@@ -3,8 +3,6 @@
\def\isabellecontext{Inner{\isacharunderscore}Syntax}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -392,7 +390,7 @@
\end{matharray}
\begin{rail}
- ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
+ ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
;
\end{rail}
@@ -551,13 +549,15 @@
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\
- & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid{\isachardoublequote}} \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
- \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
+ \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\
+ & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
\end{supertabular}
\end{center}
--- a/doc-src/IsarRef/Thy/document/Introduction.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Sun Feb 15 18:56:13 2009 +0100
@@ -30,27 +30,27 @@
The \emph{Isabelle} system essentially provides a generic
infrastructure for building deductive systems (programmed in
Standard ML), with a special focus on interactive theorem proving in
- higher-order logics. In the olden days even end-users would refer
- to certain ML functions (goal commands, tactics, tacticals etc.) to
- pursue their everyday theorem proving tasks
- \cite{isabelle-intro,isabelle-ref}.
+ higher-order logics. Many years ago, even end-users would refer to
+ certain ML functions (goal commands, tactics, tacticals etc.) to
+ pursue their everyday theorem proving tasks.
In contrast \emph{Isar} provides an interpreted language environment
of its own, which has been specifically tailored for the needs of
theory and proof development. Compared to raw ML, the Isabelle/Isar
top-level provides a more robust and comfortable development
- platform, with proper support for theory development graphs,
- single-step transactions with unlimited undo, etc. The
- Isabelle/Isar version of the \emph{Proof~General} user interface
- \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
- front-end for interactive theory and proof development in this
- advanced theorem proving environment.
+ platform, with proper support for theory development graphs, managed
+ transactions with unlimited undo etc. The Isabelle/Isar version of
+ the \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
+ for interactive theory and proof development in this advanced
+ theorem proving environment, even though it is somewhat biased
+ towards old-style proof scripts.
\medskip Apart from the technical advances over bare-bones ML
programming, the main purpose of the Isar language is to provide a
conceptually different view on machine-checked proofs
- \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
- ``Intelligible semi-automated reasoning''. Drawing from both the
+ \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
+ \emph{Intelligible semi-automated reasoning}. Drawing from both the
traditions of informal mathematical proof texts and high-level
programming languages, Isar offers a versatile environment for
structured formal proof documents. Thus properly written Isar
@@ -65,15 +65,15 @@
Despite its grand design of structured proof texts, Isar is able to
assimilate the old tactical style as an ``improper'' sub-language.
This provides an easy upgrade path for existing tactic scripts, as
- well as additional means for interactive experimentation and
- debugging of structured proofs. Isabelle/Isar supports a broad
- range of proof styles, both readable and unreadable ones.
+ well as some means for interactive experimentation and debugging of
+ structured proofs. Isabelle/Isar supports a broad range of proof
+ styles, both readable and unreadable ones.
\medskip The generic Isabelle/Isar framework (see
- \chref{ch:isar-framework}) should work reasonably well for any
- Isabelle object-logic that conforms to the natural deduction view of
- the Isabelle/Pure framework. Specific language elements introduced
- by the major object-logics are described in \chref{ch:hol}
+ \chref{ch:isar-framework}) works reasonably well for any Isabelle
+ object-logic that conforms to the natural deduction view of the
+ Isabelle/Pure framework. Specific language elements introduced by
+ the major object-logics are described in \chref{ch:hol}
(Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
(Isabelle/ZF). The main language elements are already provided by
the Isabelle/Pure framework. Nevertheless, examples given in the
@@ -90,207 +90,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{User interfaces%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Terminal sessions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The Isabelle \texttt{tty} tool provides a very interface for running
- the Isar interaction loop, with some support for command line
- editing. For example:
-\begin{ttbox}
-isabelle tty\medskip
-{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
-theory Foo imports Main begin;
-definition foo :: nat where "foo == 1";
-lemma "0 < foo" by (simp add: foo_def);
-end;
-\end{ttbox}
-
- Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.
- See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
- comprehensive overview of available commands and other language
- elements.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Emacs Proof General%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Plain TTY-based interaction as above used to be quite feasible with
- traditional tactic based theorem proving, but developing Isar
- documents really demands some better user-interface support. The
- Proof~General environment by David Aspinall
- \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
- interface for interactive theorem provers that organizes all the
- cut-and-paste and forward-backward walk through the text in a very
- neat way. In Isabelle/Isar, the current position within a partial
- proof document is equally important than the actual proof state.
- Thus Proof~General provides the canonical working environment for
- Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
- existing Isar documents) and for production work.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Proof~General as default Isabelle interface%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The Isabelle interface wrapper script provides an easy way to invoke
- Proof~General (including XEmacs or GNU Emacs). The default
- configuration of Isabelle is smart enough to detect the
- Proof~General distribution in several canonical places (e.g.\
- \verb|$ISABELLE_HOME/contrib/ProofGeneral|). Thus the
- capital \verb|Isabelle| executable would already refer to the
- \verb|ProofGeneral/isar| interface without further ado. The
- Isabelle interface script provides several options; pass \verb|-?| to see its usage.
-
- With the proper Isabelle interface setup, Isar documents may now be edited by
- visiting appropriate theory files, e.g.\
-\begin{ttbox}
-Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
-\end{ttbox}
- Beginners may note the tool bar for navigating forward and backward
- through the text (this depends on the local Emacs installation).
- Consult the Proof~General documentation \cite{proofgeneral} for
- further basic command sequences, in particular ``\verb|C-c C-return|''
- and ``\verb|C-c u|''.
-
- \medskip Proof~General may be also configured manually by giving
- Isabelle settings like this (see also \cite{isabelle-sys}):
-
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
- You may have to change \verb|$ISABELLE_HOME/contrib/ProofGeneral| to the actual installation
- directory of Proof~General.
-
- \medskip Apart from the Isabelle command line, defaults for
- interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
- setting. For example, the Emacs executable to be used may be
- configured in Isabelle's settings like this:
-\begin{ttbox}
-PROOFGENERAL_OPTIONS="-p xemacs-mule"
-\end{ttbox}
-
- Occasionally, a user's \verb|~/.emacs| file contains code
- that is incompatible with the (X)Emacs version used by
- Proof~General, causing the interface startup to fail prematurely.
- Here the \verb|-u false| option helps to get the interface
- process up and running. Note that additional Lisp customization
- code may reside in \verb|proofgeneral-settings.el| of
- \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The X-Symbol package%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Proof~General incorporates a version of the Emacs X-Symbol package
- \cite{x-symbol}, which handles proper mathematical symbols displayed
- on screen. Pass option \verb|-x true| to the Isabelle
- interface script, or check the appropriate Proof~General menu
- setting by hand. The main challenge of getting X-Symbol to work
- properly is the underlying (semi-automated) X11 font setup.
-
- \medskip Using proper mathematical symbols in Isabelle theories can
- be very convenient for readability of large formulas. On the other
- hand, the plain ASCII sources easily become somewhat unintelligible.
- For example, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according
- the default set of Isabelle symbols. Nevertheless, the Isabelle
- document preparation system (see \chref{ch:document-prep}) will be
- happy to print non-ASCII symbols properly. It is even possible to
- invent additional notation beyond the display capabilities of Emacs
- and X-Symbol.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Isabelle/Isar theories%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle/Isar offers the following main improvements over classic
- Isabelle.
-
- \begin{enumerate}
-
- \item A \emph{theory format} that integrates specifications and
- proofs, supporting interactive development and unlimited undo
- operation.
-
- \item A \emph{formal proof document language} designed to support
- intelligible semi-automated reasoning. Instead of putting together
- unreadable tactic scripts, the author is enabled to express the
- reasoning in way that is close to usual mathematical practice. The
- old tactical style has been assimilated as ``improper'' language
- elements.
-
- \item A simple document preparation system, for typesetting formal
- developments together with informal text. The resulting
- hyper-linked PDF documents are equally well suited for WWW
- presentation and as printed copies.
-
- \end{enumerate}
-
- The Isar proof language is embedded into the new theory format as a
- proper sub-language. Proof mode is entered by stating some
- \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
- left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
- A few theory specification mechanisms also require some proof, such
- as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
- representing sets.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This is one of the key questions, of course. First of all, the
- tactic script emulation of Isabelle/Isar essentially provides a
- clarified version of the very same unstructured proof style of
- classic Isabelle. Old-time users should quickly become acquainted
- with that (slightly degenerative) view of Isar.
-
- Writing \emph{proper} Isar proof texts targeted at human readers is
- quite different, though. Experienced users of the unstructured
- style may even have to unlearn some of their habits to master proof
- composition in Isar. In contrast, new users with less experience in
- old-style tactical proving, but a good understanding of mathematical
- proof in general, often get started easier.
-
- \medskip The present text really is only a reference manual on
- Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
- give some clues of how the concepts introduced here may be put into
- practice. Especially note that \appref{ap:refcard} provides a quick
- reference card of the most common Isabelle/Isar language elements.
-
- Further issues concerning the Isar concepts are covered in the
- literature
- \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
- The author's PhD thesis \cite{Wenzel-PhD} presently provides the
- most complete exposition of Isar foundations, techniques, and
- applications. A number of example applications are distributed with
- Isabelle, and available via the Isabelle WWW library (e.g.\
- \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
- Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
- examples, both in proper Isar proof style and unstructured tactic
- scripts.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarRef/Thy/document/Proof.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Sun Feb 15 18:56:13 2009 +0100
@@ -3,8 +3,6 @@
\def\isabellecontext{Proof}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -20,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Proofs%
+\isamarkupchapter{Proofs \label{ch:proofs}%
}
\isamarkuptrue%
%
@@ -28,8 +26,8 @@
Proof commands perform transitions of Isar/VM machine
configurations, which are block-structured, consisting of a stack of
nodes with three main components: logical proof context, current
- facts, and open goals. Isar/VM transitions are \emph{typed}
- according to the following three different modes of operation:
+ facts, and open goals. Isar/VM transitions are typed according to
+ the following three different modes of operation:
\begin{description}
@@ -49,13 +47,17 @@
\end{description}
- The proof mode indicator may be read as a verb telling the writer
- what kind of operation may be performed next. The corresponding
- typings of proof commands restricts the shape of well-formed proof
- texts to particular command sequences. So dynamic arrangements of
- commands eventually turn out as static texts of a certain structure.
- \Appref{ap:refcard} gives a simplified grammar of the overall
- (extensible) language emerging that way.%
+ The proof mode indicator may be understood as an instruction to the
+ writer, telling what kind of operation may be performed next. The
+ corresponding typings of proof commands restricts the shape of
+ well-formed proof texts to particular command sequences. So dynamic
+ arrangements of commands eventually turn out as static texts of a
+ certain structure.
+
+ \Appref{ap:refcard} gives a simplified grammar of the (extensible)
+ language emerging that way from the different types of proof
+ commands. The main ideas of the overall Isar framework are
+ explained in \chref{ch:isar-framework}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Feb 15 18:56:13 2009 +0100
@@ -22,6 +22,23 @@
}
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+The Isabelle/Isar theory format integrates specifications and
+ proofs, supporting interactive development with unlimited undo
+ operation. There is an integrated document preparation system (see
+ \chref{ch:document-prep}), for typesetting formal developments
+ together with informal text. The resulting hyper-linked PDF
+ documents can be used both for WWW presentation and printed copies.
+
+ The Isar proof language (see \chref{ch:proofs}) is embedded into the
+ theory language as a proper sub-language. Proof mode is entered by
+ stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory
+ level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}). Some theory specification mechanisms also require a proof,
+ such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of
+ the representing sets.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Defining theories \label{sec:begin-thy}%
}
\isamarkuptrue%
@@ -127,8 +144,9 @@
\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
theory itself (\secref{sec:begin-thy}).
- \item \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}} given after any local theory command
- specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
+ \item \isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isachardoublequote}c{\isacharparenright}{\isachardoublequote}} given after any
+ local theory command specifies an immediate target, e.g.\
+ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or
global theory context; the current target context will be suspended
for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
always produce a global result independently of the current target