tuned;
authorwenzelm
Thu Mar 07 19:04:00 2002 +0100 (2002-03-07)
changeset 13039cfcc1f6f21df
parent 13038 e968745986f1
child 13040 02bfd6d622ca
tuned;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/intro.tex
doc-src/IsarRef/logics.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/syntax.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Mar 07 12:03:43 2002 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Mar 07 19:04:00 2002 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4    of this class.
     1.5    
     1.6    The ``axioms'' are stored as theorems according to the given name
     1.7 -  specifications, adding the class name $c$ as name space prefix; these facts
     1.8 -  are stored collectively as $c{\dtt}axioms$, too.
     1.9 +  specifications, adding the class name $c$ as name space prefix; the same
    1.10 +  facts are also stored collectively as $c{\dtt}axioms$.
    1.11    
    1.12  \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
    1.13    goal stating a class relation or type arity.  The proof would usually
     2.1 --- a/doc-src/IsarRef/intro.tex	Thu Mar 07 12:03:43 2002 +0100
     2.2 +++ b/doc-src/IsarRef/intro.tex	Thu Mar 07 19:04:00 2002 +0100
     2.3 @@ -14,24 +14,25 @@
     2.4  own, which has been specifically tailored for the needs of theory and proof
     2.5  development.  Compared to raw ML, the Isabelle/Isar top-level provides a more
     2.6  robust and comfortable development platform, with proper support for theory
     2.7 -development graphs, single-step evaluation with unlimited undo, etc.  The
     2.8 +development graphs, single-step transactions with unlimited undo, etc.  The
     2.9  Isabelle/Isar version of the \emph{Proof~General} user interface
    2.10  \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
    2.11 -interactive theory and proof development.
    2.12 +interactive theory and proof development in this advanced theorem proving
    2.13 +environment.
    2.14  
    2.15 -\medskip Apart from these technical advances over bare-bones ML programming,
    2.16 -the main intention of Isar is to provide a conceptually different view on
    2.17 -machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD} --- ``Isar'' stands
    2.18 -for ``Intelligible semi-automated reasoning''.  Drawing from both the
    2.19 +\medskip Apart from the technical advances over bare-bones ML programming, the
    2.20 +main purpose of the Isar language is to provide a conceptually different view
    2.21 +on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar''
    2.22 +stands for ``Intelligible semi-automated reasoning''.  Drawing from both the
    2.23  traditions of informal mathematical proof texts and high-level programming
    2.24 -languages, Isar provides a versatile environment for structured formal proof
    2.25 -documents.  Thus properly written Isar proof texts become accessible to a
    2.26 -broader audience than unstructured tactic scripts (which typically only
    2.27 -provide operational information for the machine).  Writing human-readable
    2.28 -proof texts certainly requires some additional efforts by the writer in order
    2.29 -to achieve a good presentation --- both of formal and informal parts of the
    2.30 -text.  On the other hand, human-readable formal texts gain some value in their
    2.31 -own right, independently of the mechanic proof-checking process.
    2.32 +languages, Isar offers a versatile environment for structured formal proof
    2.33 +documents.  Thus properly written Isar proofs become accessible to a broader
    2.34 +audience than unstructured tactic scripts (which typically only provide
    2.35 +operational information for the machine).  Writing human-readable proof texts
    2.36 +certainly requires some additional efforts by the writer to achieve a good
    2.37 +presentation, both of formal and informal parts of the text.  On the other
    2.38 +hand, human-readable formal texts gain some value in their own right,
    2.39 +independently of the mechanic proof-checking process.
    2.40  
    2.41  Despite its grand design of structured proof texts, Isar is able to assimilate
    2.42  the old tactical style as an ``improper'' sub-language.  This provides an easy
    2.43 @@ -87,7 +88,7 @@
    2.44  \subsubsection{Proof~General as default Isabelle interface}
    2.45  
    2.46  The Isabelle interface wrapper script provides an easy way to invoke
    2.47 -Proof~General (and XEmacs or GNU Emacs).  The default configuration of
    2.48 +Proof~General (including XEmacs or GNU Emacs).  The default configuration of
    2.49  Isabelle is smart enough to detect the Proof~General distribution in several
    2.50  canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus
    2.51  the capital \texttt{Isabelle} executable would already refer to the
    2.52 @@ -101,8 +102,8 @@
    2.53  \begin{ttbox}
    2.54  Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
    2.55  \end{ttbox}
    2.56 -Users may note the tool bar for navigating forward and backward through the
    2.57 -text (this depends on the local Emacs installation).  Consult the
    2.58 +Beginners may note the tool bar for navigating forward and backward through
    2.59 +the text (this depends on the local Emacs installation).  Consult the
    2.60  Proof~General documentation \cite{proofgeneral} for further basic command
    2.61  sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
    2.62  
    2.63 @@ -164,16 +165,21 @@
    2.64  
    2.65  Isabelle/Isar offers the following main improvements over classic Isabelle.
    2.66  \begin{enumerate}
    2.67 +  
    2.68  \item A new \emph{theory format}, occasionally referred to as ``new-style
    2.69    theories'', supporting interactive development and unlimited undo operation.
    2.70 +  
    2.71  \item A \emph{formal proof document language} designed to support intelligible
    2.72    semi-automated reasoning.  Instead of putting together unreadable tactic
    2.73    scripts, the author is enabled to express the reasoning in way that is close
    2.74 -  to usual mathematical practice.
    2.75 +  to usual mathematical practice.  The old tactical style has been assimilated
    2.76 +  as ``improper'' language elements.
    2.77 +  
    2.78  \item A simple document preparation system, for typesetting formal
    2.79    developments together with informal text.  The resulting hyper-linked PDF
    2.80    documents are equally well suited for WWW presentation and as printed
    2.81    copies.
    2.82 +
    2.83  \end{enumerate}
    2.84  
    2.85  The Isar proof language is embedded into the new theory format as a proper
    2.86 @@ -186,11 +192,11 @@
    2.87  New-style theory files may still be associated with separate ML files
    2.88  consisting of plain old tactic scripts.  There is no longer any ML binding
    2.89  generated for the theory and theorems, though.  ML functions \texttt{theory},
    2.90 -\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
    2.91 -Nevertheless, migration between classic Isabelle and Isabelle/Isar is
    2.92 -relatively easy.  Thus users may start to benefit from interactive theory
    2.93 -development and document preparation, even before they have any idea of the
    2.94 -Isar proof language at all.
    2.95 +\texttt{thm}, and \texttt{thms} retrieve this information from the context
    2.96 +\cite{isabelle-ref}.  Nevertheless, migration between classic Isabelle and
    2.97 +Isabelle/Isar is relatively easy.  Thus users may start to benefit from
    2.98 +interactive theory development and document preparation, even before they have
    2.99 +any idea of the Isar proof language at all.
   2.100  
   2.101  \begin{warn}
   2.102    Proof~General does \emph{not} support mixed interactive development of
   2.103 @@ -210,9 +216,9 @@
   2.104  \subsection{Document preparation}\label{sec:document-prep}
   2.105  
   2.106  Isabelle/Isar provides a simple document preparation system based on existing
   2.107 -PDF-\LaTeX technology, with full support of hyper-links (both local references
   2.108 -and URLs), bookmarks, and thumbnails.  Thus the results are equally well
   2.109 -suited for WWW browsing and as printed copies.
   2.110 +{PDF-\LaTeX} technology, with full support of hyper-links (both local
   2.111 +references and URLs), bookmarks, and thumbnails.  Thus the results are equally
   2.112 +well suited for WWW browsing and as printed copies.
   2.113  
   2.114  \medskip
   2.115  
   2.116 @@ -245,8 +251,8 @@
   2.117  
   2.118  You may also consider to tune the \texttt{usedir} options in
   2.119  \texttt{IsaMakefile}, for example to change the output format from
   2.120 -\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D generated} option in
   2.121 -order to keep a second copy of the generated {\LaTeX} sources.
   2.122 +\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
   2.123 +second copy of the generated {\LaTeX} sources.
   2.124  
   2.125  \medskip
   2.126  
   2.127 @@ -260,13 +266,13 @@
   2.128  This is one of the key questions, of course.  First of all, the tactic script
   2.129  emulation of Isabelle/Isar essentially provides a clarified version of the
   2.130  very same unstructured proof style of classic Isabelle.  Old-time users should
   2.131 -quickly become acquainted with that (degenerative) view of Isar at the least.
   2.132 +quickly become acquainted with that (slightly degenerative) view of Isar.
   2.133  
   2.134  Writing \emph{proper} Isar proof texts targeted at human readers is quite
   2.135  different, though.  Experienced users of the unstructured style may even have
   2.136  to unlearn some of their habits to master proof composition in Isar.  In
   2.137  contrast, new users with less experience in old-style tactical proving, but a
   2.138 -good understanding of mathematical proof in general often get started easier.
   2.139 +good understanding of mathematical proof in general, often get started easier.
   2.140  
   2.141  \medskip The present text really is only a reference manual on Isabelle/Isar,
   2.142  not a tutorial.  Nevertheless, we will attempt to give some clues of how the
     3.1 --- a/doc-src/IsarRef/logics.tex	Thu Mar 07 12:03:43 2002 +0100
     3.2 +++ b/doc-src/IsarRef/logics.tex	Thu Mar 07 19:04:00 2002 +0100
     3.3 @@ -1,5 +1,5 @@
     3.4  
     3.5 -\chapter{Object-logic specific elements}\label{ch:logics}
     3.6 +\chapter{Object-logic Specific Elements}\label{ch:logics}
     3.7  
     3.8  \section{General logic setup}\label{sec:object-logic}
     3.9  
    3.10 @@ -82,7 +82,7 @@
    3.11  
    3.12  \section{HOL}
    3.13  
    3.14 -\subsection{Primitive types}\label{sec:typedef}
    3.15 +\subsection{Primitive types}\label{sec:hol-typedef}
    3.16  
    3.17  \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef}
    3.18  \begin{matharray}{rcl}
    3.19 @@ -167,7 +167,7 @@
    3.20  \end{descr}
    3.21  
    3.22  
    3.23 -\section{Records}\label{sec:hol-record}
    3.24 +\subsection{Records}\label{sec:hol-record}
    3.25  
    3.26  In principle, records merely generalize the concept of tuples where components
    3.27  may be addressed by labels instead of just position.  The logical
    3.28 @@ -178,7 +178,7 @@
    3.29  more details on object-oriented verification and record subtyping in HOL.
    3.30  
    3.31  
    3.32 -\subsection{Basic concepts}
    3.33 +\subsubsection{Basic concepts}
    3.34  
    3.35  Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the
    3.36  level of terms and types.  The notation is as follows:
    3.37 @@ -235,7 +235,7 @@
    3.38  practice.
    3.39  
    3.40  
    3.41 -\subsection{Record specifications}\label{sec:hol-record-def}
    3.42 +\subsubsection{Record specifications}\label{sec:hol-record-def}
    3.43  
    3.44  \indexisarcmdof{HOL}{record}
    3.45  \begin{matharray}{rcl}
    3.46 @@ -271,7 +271,7 @@
    3.47  
    3.48  \end{descr}
    3.49  
    3.50 -\subsection{Record operations}\label{sec:hol-record-ops}
    3.51 +\subsubsection{Record operations}\label{sec:hol-record-ops}
    3.52  
    3.53  Any record definition of the form presented above produces certain standard
    3.54  operations.  Selectors and updates are provided for any field, including the
    3.55 @@ -339,7 +339,7 @@
    3.56  \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
    3.57  
    3.58  
    3.59 -\subsection{Derived rules and proof tools}\label{sec:hol-record-thms}
    3.60 +\subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
    3.61  
    3.62  The record package proves several results internally, declaring these facts to
    3.63  appropriate proof tools.  This enables users to reason about record structures
    3.64 @@ -642,7 +642,7 @@
    3.65  \end{descr}
    3.66  
    3.67  
    3.68 -\subsection{Generating executable code}
    3.69 +\subsection{Executable code}
    3.70  
    3.71  Isabelle/Pure provides a generic infrastructure to support code generation
    3.72  from executable specifications, both functional and relational programs.
     4.1 --- a/doc-src/IsarRef/pure.tex	Thu Mar 07 12:03:43 2002 +0100
     4.2 +++ b/doc-src/IsarRef/pure.tex	Thu Mar 07 19:04:00 2002 +0100
     4.3 @@ -1,8 +1,8 @@
     4.4  
     4.5  \chapter{Basic Language Elements}\label{ch:pure-syntax}
     4.6  
     4.7 -Subsequently, we introduce the main part of Pure Isar theory and proof
     4.8 -commands, together with fundamental proof methods and attributes.
     4.9 +Subsequently, we introduce the main part of Pure theory and proof commands,
    4.10 +together with fundamental proof methods and attributes.
    4.11  Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
    4.12  tools and packages (such as the Simplifier) that are either part of Pure
    4.13  Isabelle or pre-installed in most object logics.  Chapter~\ref{ch:logics}
    4.14 @@ -14,9 +14,10 @@
    4.15  \emph{improper commands}.  Some proof methods and attributes introduced later
    4.16  are classified as improper as well.  Improper Isar language elements, which
    4.17  are subsequently marked by ``$^*$'', are often helpful when developing proof
    4.18 -documents, while their use is discouraged for the final outcome.  Typical
    4.19 -examples are diagnostic commands that print terms or theorems according to the
    4.20 -current context; other commands emulate old-style tactical theorem proving.
    4.21 +documents, while their use is discouraged for the final human-readable
    4.22 +outcome.  Typical examples are diagnostic commands that print terms or
    4.23 +theorems according to the current context; other commands emulate old-style
    4.24 +tactical theorem proving.
    4.25  
    4.26  
    4.27  \section{Theory commands}
    4.28 @@ -42,8 +43,8 @@
    4.29  there may be an optional $\isarkeyword{header}$ declaration, which is relevant
    4.30  to document preparation only; it acts very much like a special pre-theory
    4.31  markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The
    4.32 -$\END$ commands concludes a theory development; it has to be the very last
    4.33 -command of any theory file to loaded in batch-mode.  The theory context may be
    4.34 +$\END$ command concludes a theory development; it has to be the very last
    4.35 +command of any theory file loaded in batch-mode.  The theory context may be
    4.36  also changed interactively by $\CONTEXT$ without creating a new theory.
    4.37  
    4.38  \begin{rail}
    4.39 @@ -206,21 +207,27 @@
    4.40  \end{rail}
    4.41  
    4.42  \begin{descr}
    4.43 +
    4.44  \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
    4.45    $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
    4.46    as are available in Isabelle/HOL for example, type synonyms are just purely
    4.47    syntactic abbreviations without any logical significance.  Internally, type
    4.48    synonyms are fully expanded.
    4.49 +  
    4.50  \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
    4.51 -  $t$, intended as an actual logical type.  Note that object-logics such as
    4.52 -  Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
    4.53 +  $t$, intended as an actual logical type.  Note that the Isabelle/HOL
    4.54 +  object-logic overrides $\isarkeyword{typedecl}$ by its own version
    4.55 +  (\S\ref{sec:hol-typedef}).
    4.56 +
    4.57  \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
    4.58    $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
    4.59    Isabelle's inner syntax of terms or types.
    4.60 +
    4.61  \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
    4.62    signature of types by new type constructor arities.  This is done
    4.63    axiomatically!  The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
    4.64    way to introduce proven type arities.
    4.65 +
    4.66  \end{descr}
    4.67  
    4.68  
    4.69 @@ -332,7 +339,7 @@
    4.70    
    4.71    Axioms are usually only introduced when declaring new logical systems.
    4.72    Everyday work is typically done the hard way, with proper definitions and
    4.73 -  actual proven theorems.
    4.74 +  proven theorems.
    4.75    
    4.76  \item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
    4.77    in the theory context, or the specified locale (see also
    4.78 @@ -454,11 +461,11 @@
    4.79  }
    4.80  
    4.81  Note that mere tactic emulations may ignore the \texttt{facts} parameter
    4.82 -above.  Proper proof methods would do something ``appropriate'' with the list
    4.83 -of current facts, though.  Single-rule methods usually do strict
    4.84 -forward-chaining (e.g.\ by using \texttt{Method.multi_resolves}), while
    4.85 -automatic ones just insert the facts using \texttt{Method.insert_tac} before
    4.86 -applying the main tactic.
    4.87 +above.  Proper proof methods would do something appropriate with the list of
    4.88 +current facts, though.  Single-rule methods usually do strict forward-chaining
    4.89 +(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just
    4.90 +insert the facts using \texttt{Method.insert_tac} before applying the main
    4.91 +tactic.
    4.92  \end{descr}
    4.93  
    4.94  
    4.95 @@ -564,8 +571,8 @@
    4.96  operation may be performed next.  The corresponding typings of proof commands
    4.97  restricts the shape of well-formed proof texts to particular command
    4.98  sequences.  So dynamic arrangements of commands eventually turn out as static
    4.99 -texts.  Appendix~\ref{ap:refcard} gives a simplified grammar of the overall
   4.100 -(extensible) language emerging that way.
   4.101 +texts of a certain structure.  Appendix~\ref{ap:refcard} gives a simplified
   4.102 +grammar of the overall (extensible) language emerging that way.
   4.103  
   4.104  
   4.105  \subsection{Markup commands}\label{sec:markup-prf}
   4.106 @@ -605,11 +612,11 @@
   4.107  The logical proof context consists of fixed variables and assumptions.  The
   4.108  former closely correspond to Skolem constants, or meta-level universal
   4.109  quantification as provided by the Isabelle/Pure logical framework.
   4.110 -Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
   4.111 -a local value that may be used in the subsequent proof as any other variable
   4.112 -or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
   4.113 -context will be universally closed wrt.\ $x$ at the outermost level: $\edrv
   4.114 -\All x \phi$ (this is expressed using Isabelle's meta-variables).
   4.115 +Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results
   4.116 +in a local value that may be used in the subsequent proof as any other
   4.117 +variable or constant.  Furthermore, any result $\edrv \phi[x]$ exported from
   4.118 +the context will be universally closed wrt.\ $x$ at the outermost level:
   4.119 +$\edrv \All x \phi$ (this is expressed using Isabelle's meta-variables).
   4.120  
   4.121  Similarly, introducing some assumption $\chi$ has two effects.  On the one
   4.122  hand, a local theorem is created that may be used as a fact in subsequent
   4.123 @@ -622,8 +629,8 @@
   4.124  $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
   4.125  user.
   4.126  
   4.127 -Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
   4.128 -combining $\FIX x$ with another version of assumption that causes any
   4.129 +Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by
   4.130 +combining ``$\FIX x$'' with another version of assumption that causes any
   4.131  hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
   4.132  Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
   4.133  
   4.134 @@ -640,8 +647,10 @@
   4.135  \end{rail}
   4.136  
   4.137  \begin{descr}
   4.138 +  
   4.139  \item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
   4.140    $\vec x$.
   4.141 +  
   4.142  \item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
   4.143    theorems $\vec\phi$ by assumption.  Subsequent results applied to an
   4.144    enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
   4.145 @@ -651,12 +660,14 @@
   4.146    Several lists of assumptions may be given (separated by
   4.147    $\isarkeyword{and}$); the resulting list of current facts consists of all of
   4.148    these concatenated.
   4.149 +  
   4.150  \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
   4.151    In results exported from the context, $x$ is replaced by $t$.  Basically,
   4.152 -  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the
   4.153 -  resulting hypothetical equation solved by reflexivity.
   4.154 +  ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
   4.155 +  with the resulting hypothetical equation solved by reflexivity.
   4.156    
   4.157    The default name for the definitional equation is $x_def$.
   4.158 +
   4.159  \end{descr}
   4.160  
   4.161  The special name $prems$\indexisarthm{prems} refers to all assumptions of the
   4.162 @@ -679,10 +690,10 @@
   4.163  Any fact will usually be involved in further proofs, either as explicit
   4.164  arguments of proof methods, or when forward chaining towards the next goal via
   4.165  $\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms
   4.166 -involving $\NOTE$.  The $\USINGNAME$ elements allows to augment the collection
   4.167 -of used facts \emph{after} a goal has been stated.  Note that the special
   4.168 -theorem name $this$\indexisarthm{this} refers to the most recently established
   4.169 -facts, but only \emph{before} issuing a follow-up claim.
   4.170 +involving $\NOTENAME$.  The $\USINGNAME$ elements augments the collection of
   4.171 +used facts \emph{after} a goal has been stated.  Note that the special theorem
   4.172 +name $this$\indexisarthm{this} refers to the most recently established facts,
   4.173 +but only \emph{before} issuing a follow-up claim.
   4.174  
   4.175  \begin{rail}
   4.176    'note' (thmdef? thmrefs + 'and')
   4.177 @@ -692,28 +703,35 @@
   4.178  \end{rail}
   4.179  
   4.180  \begin{descr}
   4.181 +
   4.182  \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
   4.183    as $a$.  Note that attributes may be involved as well, both on the left and
   4.184    right hand sides.
   4.185 +
   4.186  \item [$\THEN$] indicates forward chaining by the current facts in order to
   4.187    establish the goal to be claimed next.  The initial proof method invoked to
   4.188 -  refine that will be offered the facts to do ``anything appropriate'' (cf.\ 
   4.189 +  refine that will be offered the facts to do ``anything appropriate'' (see
   4.190    also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
   4.191    \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
   4.192    introduction.  Automatic methods usually insert the facts into the goal
   4.193    state before operation.  This provides a simple scheme to control relevance
   4.194    of facts in automated proof search.
   4.195 -\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
   4.196 -  equivalent to $\FROM{this}$.
   4.197 -\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward
   4.198 -  chaining is from earlier facts together with the current ones.
   4.199 +  
   4.200 +\item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$
   4.201 +  is equivalent to ``$\FROM{this}$''.
   4.202 +  
   4.203 +\item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
   4.204 +  forward chaining is from earlier facts together with the current ones.
   4.205 +  
   4.206  \item [$\USING{\vec b}$] augments the facts being currently indicated for use
   4.207 -  in a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
   4.208 +  by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
   4.209 +
   4.210  \end{descr}
   4.211  
   4.212 -Forward chaining with an empty list of theorems is the same as not chaining.
   4.213 -Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
   4.214 -since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems.
   4.215 +Forward chaining with an empty list of theorems is the same as not chaining at
   4.216 +all.  Thus ``$\FROM{nothing}$'' has no effect apart from entering
   4.217 +$prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the
   4.218 +empty list of theorems.
   4.219  
   4.220  Basic proof methods (such as $rule$) expect multiple facts to be given in
   4.221  their proper order, corresponding to a prefix of the premises of the rule
   4.222 @@ -742,18 +760,18 @@
   4.223  \end{matharray}
   4.224  
   4.225  From a theory context, proof mode is entered by an initial goal command such
   4.226 -as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$.  Within a proof, new claims
   4.227 -may be introduced locally as well; four variants are available here to
   4.228 +as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$.  Within a proof, new
   4.229 +claims may be introduced locally as well; four variants are available here to
   4.230  indicate whether forward chaining of facts should be performed initially (via
   4.231 -$\THEN$), and whether the emerging result is meant to solve some pending goal.
   4.232 +$\THEN$), and whether the final result is meant to solve some pending goal.
   4.233  
   4.234  Goals may consist of multiple statements, resulting in a list of facts
   4.235  eventually.  A pending multi-goal is internally represented as a meta-level
   4.236 -conjunction (printed as \verb,&&,), which is automatically split into the
   4.237 -corresponding number of sub-goals prior to any initial method application, via
   4.238 +conjunction (printed as \verb,&&,), which is usually split into the
   4.239 +corresponding number of sub-goals prior to an initial method application, via
   4.240  $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
   4.241 -(\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
   4.242 -  \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
   4.243 +(\S\ref{sec:tactic-commands}).  The $induct$ method covered in
   4.244 +\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.
   4.245  
   4.246  Claims at the theory level may be either in short or long form.  A short goal
   4.247  merely consists of several simultaneous propositions (often just one).  A long
   4.248 @@ -775,13 +793,13 @@
   4.249  \end{rail}
   4.250  
   4.251  \begin{descr}
   4.252 +  
   4.253  \item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
   4.254    eventually resulting in some fact $\turn \vec\phi$ to be put back into the
   4.255 -  theory context, and optionally into the specified locale, cf.\ 
   4.256 -  \S\ref{sec:locale}.  An additional \railnonterm{context} specification may
   4.257 -  build an initial proof context for the subsequent claim; this may include
   4.258 -  local definitions and syntax as well, see the definition of $contextelem$ in
   4.259 -  \S\ref{sec:locale}.
   4.260 +  theory context, or into the specified locale (cf.\ \S\ref{sec:locale}).  An
   4.261 +  additional \railnonterm{context} specification may build up an initial proof
   4.262 +  context for the subsequent claim; this includes local definitions and syntax
   4.263 +  as well, see the definition of $contextelem$ in \S\ref{sec:locale}.
   4.264    
   4.265  \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
   4.266    the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
   4.267 @@ -796,27 +814,29 @@
   4.268  \item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage
   4.269    to refine some pending sub-goal for each one of the finished result, after
   4.270    having been exported into the corresponding context (at the head of the
   4.271 -  sub-proof that the $\SHOWNAME$ command belongs to).
   4.272 +  sub-proof of this $\SHOWNAME$ command).
   4.273    
   4.274    To accommodate interactive debugging, resulting rules are printed before
   4.275    being applied internally.  Even more, interactive execution of $\SHOWNAME$
   4.276 -  predicts potential failure after finishing its proof, and displays the
   4.277 -  resulting error message as a warning beforehand, adding this header:
   4.278 +  predicts potential failure and displays the resulting error as a warning
   4.279 +  beforehand.  Watch out for the following message:
   4.280  
   4.281    \begin{ttbox}
   4.282    Problem! Local statement will fail to solve any pending goal
   4.283    \end{ttbox}
   4.284 +  
   4.285 +\item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local
   4.286 +  goal to be proven by forward chaining the current facts.  Note that
   4.287 +  $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''.
   4.288 +  
   4.289 +\item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''.  Note that $\THUSNAME$
   4.290 +  is also equivalent to ``$\FROM{this}~\SHOWNAME$''.
   4.291  
   4.292 -\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
   4.293 -  to be proven by forward chaining the current facts.  Note that $\HENCENAME$
   4.294 -  is also equivalent to $\FROM{this}~\HAVENAME$.
   4.295 -\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$.  Note that $\THUSNAME$ is
   4.296 -  also equivalent to $\FROM{this}~\SHOWNAME$.
   4.297  \end{descr}
   4.298  
   4.299 -Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
   4.300 -$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
   4.301 -Furthermore, the local context of a (non-atomic) goal is provided via the
   4.302 +Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
   4.303 +be bound automatically, see also \S\ref{sec:term-abbrev}.  Furthermore, the
   4.304 +local context of a (non-atomic) goal is provided via the
   4.305  $rule_context$\indexisarcase{rule-context} case, see also
   4.306  \S\ref{sec:rule-cases}.
   4.307  
   4.308 @@ -827,7 +847,7 @@
   4.309      schematic variables}, although this does not conform to the aim of
   4.310    human-readable proof documents!  The main problem with schematic goals is
   4.311    that the actual outcome is usually hard to predict, depending on the
   4.312 -  behavior of the actual proof methods applied during the reasoning.  Note
   4.313 +  behavior of the proof methods applied during the course of reasoning.  Note
   4.314    that most semi-automated methods heavily depend on several kinds of implicit
   4.315    rule declarations within the current theory context.  As this would also
   4.316    result in non-compositional checking of sub-proofs, \emph{local goals} are
   4.317 @@ -863,7 +883,7 @@
   4.318    remaining goals.  No facts are passed to $m@2$.
   4.319  \end{enumerate}
   4.320  
   4.321 -The only other proper way to affect pending goals in a proof body is by
   4.322 +The only other (proper) way to affect pending goals in a proof body is by
   4.323  $\SHOWNAME$, which involves an explicit statement of what is to be solved
   4.324  eventually.  Thus we avoid the fundamental problem of unstructured tactic
   4.325  scripts that consist of numerous consecutive goal transformations, with
   4.326 @@ -875,7 +895,7 @@
   4.327  either solve the goal completely, or constitute some well-understood reduction
   4.328  to new sub-goals.  Arbitrary automatic proof tools that are prone leave a
   4.329  large number of badly structured sub-goals are no help in continuing the proof
   4.330 -document in any intelligible way.
   4.331 +document in an intelligible manner.
   4.332  
   4.333  Unless given explicitly by the user, the default initial method is ``$rule$'',
   4.334  which applies a single standard elimination or introduction rule according to
   4.335 @@ -894,8 +914,10 @@
   4.336  \end{rail}
   4.337  
   4.338  \begin{descr}
   4.339 +  
   4.340  \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
   4.341    forward chaining are passed if so indicated by $proof(chain)$ mode.
   4.342 +  
   4.343  \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
   4.344    concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
   4.345    $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
   4.346 @@ -905,25 +927,29 @@
   4.347      ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
   4.348    context.  Debugging such a situation might involve temporarily changing
   4.349    $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
   4.350 -  some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
   4.351 +  occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
   4.352 +  
   4.353  \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
   4.354 -  abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods,
   4.355 -  though.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
   4.356 -  by expanding its definition; in many cases $\PROOF{m@1}$ is already
   4.357 -  sufficient to see what is going wrong.
   4.358 +  abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both
   4.359 +  methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
   4.360 +  by expanding its definition; in many cases $\PROOF{m@1}$ (or even
   4.361 +  $\APPLY{m@1}$) is already sufficient to see the problem.
   4.362 +
   4.363  \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
   4.364    abbreviates $\BY{rule}$.
   4.365 +
   4.366  \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
   4.367    abbreviates $\BY{this}$.
   4.368 +  
   4.369  \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve
   4.370    the pending claim without further ado.  This only works in interactive
   4.371 -  development, or if the \texttt{quick_and_dirty} flag is enabled.  Certainly,
   4.372 -  any facts emerging from fake proofs are not the real thing.  Internally,
   4.373 -  each theorem container is tainted by an oracle invocation, which is
   4.374 -  indicated as ``$[!]$'' in the printed result.
   4.375 +  development, or if the \texttt{quick_and_dirty} flag is enabled.  Facts
   4.376 +  emerging from fake proofs are not the real thing.  Internally, each theorem
   4.377 +  container is tainted by an oracle invocation, which is indicated as
   4.378 +  ``$[!]$'' in the printed result.
   4.379    
   4.380    The most important application of $\SORRY$ is to support experimentation and
   4.381 -  top-down proof development in a simple manner.
   4.382 +  top-down proof development.
   4.383  \end{descr}
   4.384  
   4.385  
   4.386 @@ -975,22 +1001,23 @@
   4.387  \item [``$-$''] does nothing but insert the forward chaining facts as premises
   4.388    into the goal.  Note that command $\PROOFNAME$ without any method actually
   4.389    performs a single reduction step using the $rule$ method; thus a plain
   4.390 -  \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
   4.391 -  alone.
   4.392 +  \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
   4.393 +  $\PROOFNAME$ alone.
   4.394    
   4.395 -\item [$assumption$] solves some goal by a single assumption step.  Any facts
   4.396 -  given (${} \le 1$) are guaranteed to participate in the refinement.  Recall
   4.397 -  that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any
   4.398 -  remaining sub-goals by assumption, so structured proofs usually need not
   4.399 -  quote the $assumption$ method at all.
   4.400 +\item [$assumption$] solves some goal by a single assumption step.  All given
   4.401 +  facts are guaranteed to participate in the refinement; this means there may
   4.402 +  be only $0$ or $1$ in the first place.  Recall that $\QEDNAME$ (see
   4.403 +  \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by
   4.404 +  assumption, so structured proofs usually need not quote the $assumption$
   4.405 +  method at all.
   4.406    
   4.407  \item [$this$] applies all of the current facts directly as rules.  Recall
   4.408 -  that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
   4.409 +  that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''.
   4.410    
   4.411  \item [$rule~\vec a$] applies some rule given as argument in backward manner;
   4.412    facts are used to reduce the rule before applying it to the goal.  Thus
   4.413 -  $rule$ without facts is plain \emph{introduction}, while with facts it
   4.414 -  becomes \emph{elimination}.
   4.415 +  $rule$ without facts is plain introduction, while with facts it becomes
   4.416 +  elimination.
   4.417    
   4.418    When no arguments are given, the $rule$ method tries to pick appropriate
   4.419    rules automatically, as declared in the current context using the $intro$,
   4.420 @@ -1001,18 +1028,18 @@
   4.421  \item [$rules$] performs intuitionistic proof search, depending on
   4.422    specifically declared rules from the context, or given as explicit
   4.423    arguments.  Chained facts are inserted into the goal before commencing proof
   4.424 -  search; $rules!$ means to include the current $prems$ as well.
   4.425 +  search; ``$rules!$'' means to include the current $prems$ as well.
   4.426    
   4.427    Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
   4.428    indicator refers to ``safe'' rules, which may be applied aggressively
   4.429    (without considering back-tracking later).  Rules declared with ``$?$'' are
   4.430    ignored in proof search (the single-step $rule$ method still observes
   4.431    these).  An explicit weight annotation may be given as well; otherwise the
   4.432 -  number of rule premises will be taken into account.
   4.433 -
   4.434 +  number of rule premises will be taken into account here.
   4.435 +  
   4.436  \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   4.437    destruct rules, to be used with the $rule$ and $rules$ methods.  Note that
   4.438 -  the latter will ignore rules declare with ``$?$'', while ``$!$'' are used
   4.439 +  the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
   4.440    most aggressively.
   4.441    
   4.442    The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
   4.443 @@ -1024,7 +1051,7 @@
   4.444  \item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
   4.445    parallel).  This corresponds to the \texttt{MRS} operator in ML
   4.446    \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
   4.447 -  skipped by including ``$\_$'' (underscore) as argument.
   4.448 +  effectively skipped by including ``$\_$'' (underscore) as argument.
   4.449    
   4.450  \item [$of~\vec t$] performs positional instantiation.  The terms $\vec t$ are
   4.451    substituted for any schematic variables occurring in a theorem from left to
   4.452 @@ -1045,8 +1072,8 @@
   4.453  
   4.454  Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
   4.455  or by annotating assumptions or goal statements with a list of patterns
   4.456 -$\ISS{p@1\;\dots}{p@n}$.  In both cases, higher-order matching is invoked to
   4.457 -bind extra-logical term variables, which may be either named schematic
   4.458 +``$\ISS{p@1\;\dots}{p@n}$''.  In both cases, higher-order matching is invoked
   4.459 +to bind extra-logical term variables, which may be either named schematic
   4.460  variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
   4.461  (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
   4.462  patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
   4.463 @@ -1058,15 +1085,15 @@
   4.464  in \emph{arbitrary} instances later.  Even though actual polymorphism should
   4.465  be rarely used in practice, this mechanism is essential to achieve proper
   4.466  incremental type-inference, as the user proceeds to build up the Isar proof
   4.467 -text.
   4.468 +text from left to right.
   4.469  
   4.470  \medskip
   4.471  
   4.472 -Term abbreviations are quite different from actual local definitions as
   4.473 -introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
   4.474 -visible within the logic as actual equations, while abbreviations disappear
   4.475 -during the input process just after type checking.  Also note that $\DEFNAME$
   4.476 -does not support polymorphism.
   4.477 +Term abbreviations are quite different from local definitions as introduced
   4.478 +via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are visible within
   4.479 +the logic as actual equations, while abbreviations disappear during the input
   4.480 +process just after type checking.  Also note that $\DEFNAME$ does not support
   4.481 +polymorphism.
   4.482  
   4.483  \begin{rail}
   4.484    'let' ((term + 'and') '=' term + 'and')
   4.485 @@ -1110,9 +1137,8 @@
   4.486  local goal statement automatically opens \emph{two} blocks, which are closed
   4.487  again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
   4.488  different context within a sub-proof may be switched via $\NEXT$, which is
   4.489 -just a single block-close followed by block-open again.  Thus the effect of
   4.490 -$\NEXT$ to reset the local proof context. There is no goal focus involved
   4.491 -here!
   4.492 +just a single block-close followed by block-open again.  The effect of $\NEXT$
   4.493 +is to reset the local proof context; there is no goal focus involved here!
   4.494  
   4.495  For slightly more advanced applications, there are explicit block parentheses
   4.496  as well.  These typically achieve a stronger forward style of reasoning.
   4.497 @@ -1183,20 +1209,19 @@
   4.498    No facts are passed to $m$.  Furthermore, the static context is that of the
   4.499    enclosing goal (as for actual $\QEDNAME$).  Thus the proof method may not
   4.500    refer to any assumptions introduced in the current body, for example.
   4.501 -
   4.502 +  
   4.503  \item [$\isarkeyword{done}$] completes a proof script, provided that the
   4.504 -  current goal state is already solved completely.  Note that actual
   4.505 -  structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to
   4.506 -  conclude proof scripts as well.
   4.507 +  current goal state is solved completely.  Note that actual structured proof
   4.508 +  commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof
   4.509 +  scripts as well.
   4.510  
   4.511  \item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list
   4.512    of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$
   4.513    by default), while $prefer$ brings goal $n$ to the top.
   4.514 -
   4.515 +  
   4.516  \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
   4.517 -  the latest proof command.\footnote{Unlike the ML function \texttt{back}
   4.518 -    \cite{isabelle-ref}, the Isar command does not search upwards for further
   4.519 -    branch points.} Basically, any proof command may return multiple results.
   4.520 +  the latest proof command.  Basically, any proof command may return multiple
   4.521 +  results.
   4.522    
   4.523  \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
   4.524    context (or the specified locale, see also \S\ref{sec:locale}).  No theorem
   4.525 @@ -1223,8 +1248,8 @@
   4.526  different from ``faking'' actual proofs via $\SORRY$ (see
   4.527  \S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
   4.528  but goes back right to the theory level.  Furthermore, $\OOPS$ does not
   4.529 -produce any result theorem --- there is no claim to be able to complete the
   4.530 -proof anyhow.
   4.531 +produce any result theorem --- there is no intended claim to be able to
   4.532 +complete the proof anyhow.
   4.533  
   4.534  A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
   4.535  system itself, in conjunction with the document preparation tools of Isabelle
   4.536 @@ -1234,8 +1259,8 @@
   4.537  ``$\OOPS$'' keyword.
   4.538  
   4.539  \medskip The $\OOPS$ command is undo-able, unlike $\isarkeyword{kill}$ (see
   4.540 -\S\ref{sec:history}).  The effect is to get back to the theory \emph{before}
   4.541 -the opening of the proof.
   4.542 +\S\ref{sec:history}).  The effect is to get back to the theory just before the
   4.543 +opening of the proof.
   4.544  
   4.545  
   4.546  \section{Other commands}
   4.547 @@ -1340,30 +1365,42 @@
   4.548  for simplifications.
   4.549  
   4.550  \begin{descr}
   4.551 +  
   4.552  \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
   4.553    including keywords and command.
   4.554 +  
   4.555  \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
   4.556    terms, depending on the current context.  The output can be very verbose,
   4.557    including grammar tables and syntax translation rules.  See \cite[\S7,
   4.558    \S8]{isabelle-ref} for further information on Isabelle's inner syntax.
   4.559 +  
   4.560  \item [$\isarkeyword{print_methods}$] prints all proof methods available in
   4.561    the current theory context.
   4.562 +  
   4.563  \item [$\isarkeyword{print_attributes}$] prints all attributes available in
   4.564    the current theory context.
   4.565 +  
   4.566  \item [$\isarkeyword{print_theorems}$] prints theorems available in the
   4.567 -  current theory context.  In interactive mode this actually refers to the
   4.568 -  theorems left by the last transaction; this allows to inspect the result of
   4.569 -  advanced definitional packages, such as $\isarkeyword{datatype}$.
   4.570 +  current theory context.
   4.571 +  
   4.572 +  In interactive mode this actually refers to the theorems left by the last
   4.573 +  transaction; this allows to inspect the result of advanced definitional
   4.574 +  packages, such as $\isarkeyword{datatype}$.
   4.575 +  
   4.576  \item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the
   4.577    theory context containing all of the constants occurring in the terms $\vec
   4.578    t$.  Note that giving the empty list yields \emph{all} theorems of the
   4.579    current theory.
   4.580 +  
   4.581  \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
   4.582    using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
   4.583 +  
   4.584  \item [$\isarkeyword{print_facts}$] prints any named facts of the current
   4.585    context, including assumptions and local results.
   4.586 +  
   4.587  \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
   4.588    the context.
   4.589 +
   4.590  \end{descr}
   4.591  
   4.592  
   4.593 @@ -1421,8 +1458,7 @@
   4.594  \end{descr}
   4.595  
   4.596  These system commands are scarcely used when working with the Proof~General
   4.597 -interface, since loading of theories is done fully transparently.
   4.598 -
   4.599 +interface, since loading of theories is done transparently.
   4.600  
   4.601  %%% Local Variables: 
   4.602  %%% mode: latex
     5.1 --- a/doc-src/IsarRef/syntax.tex	Thu Mar 07 12:03:43 2002 +0100
     5.2 +++ b/doc-src/IsarRef/syntax.tex	Thu Mar 07 19:04:00 2002 +0100
     5.3 @@ -1,5 +1,5 @@
     5.4  
     5.5 -\chapter{Syntax primitives}
     5.6 +\chapter{Syntax Primitives}
     5.7  
     5.8  The rather generic framework of Isabelle/Isar syntax emerges from three main
     5.9  syntactic categories: \emph{commands} of the top-level Isar engine (covering
    5.10 @@ -40,7 +40,7 @@
    5.11  particularly useful in interactive shell sessions to make clear where the
    5.12  current command is intended to end.  Otherwise, the interpreter loop will
    5.13  continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is
    5.14 -clearly indicated from the input syntax, e.g.\ encounter of the next command
    5.15 +clearly recognized from the input syntax, e.g.\ encounter of the next command
    5.16  keyword.
    5.17  
    5.18  Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
    5.19 @@ -92,12 +92,11 @@
    5.20    symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots
    5.21  \end{matharray}
    5.22  
    5.23 -The syntax of \railtoken{string} admits any characters, including newlines;
    5.24 -``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by
    5.25 -a backslash.  Note that ML-style control characters are \emph{not} supported.
    5.26 -The body of \railtoken{verbatim} may consist of any text not containing
    5.27 -``\verb|*}|''; this allows handsome inclusion of quotes without further
    5.28 -escapes.
    5.29 +The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
    5.30 +(double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash.
    5.31 +Note that ML-style control characters are \emph{not} supported.  The body of
    5.32 +$verbatim$ may consist of any text not containing ``\verb|*}|''; this allows
    5.33 +convenient inclusion of quotes without further escapes.
    5.34  
    5.35  Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
    5.36  just as in ML.  Note that these are \emph{source} comments only, which are
    5.37 @@ -109,7 +108,8 @@
    5.38    Proof~General does not handle nested comments properly; it is also unable to
    5.39    keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
    5.40    their rather different meaning.  These are inherent problems of Emacs
    5.41 -  legacy.
    5.42 +  legacy.  Users should not be overly aggressive about nesting or alternating
    5.43 +  these delimiters.
    5.44  \end{warn}
    5.45  
    5.46  \medskip
    5.47 @@ -209,8 +209,8 @@
    5.48  level.  Basically, any such entity has to be quoted to turn it into a single
    5.49  token (the parsing and type-checking is performed internally later).  For
    5.50  convenience, a slightly more liberal convention is adopted: quotes may be
    5.51 -omitted for any type or term that is already \emph{atomic} at the outer level.
    5.52 -For example, one may just write \texttt{x} instead of \texttt{"x"}.  Note that
    5.53 +omitted for any type or term that is already atomic at the outer level.  For
    5.54 +example, one may just write \texttt{x} instead of \texttt{"x"}.  Note that
    5.55  symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
    5.56  provided these have not been superseded by commands or other keywords already
    5.57  (e.g.\ \texttt{=} or \texttt{+}).
    5.58 @@ -338,9 +338,9 @@
    5.59  Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
    5.60  the former requires an actual singleton result.  Any of these theorem
    5.61  specifications may include lists of attributes both on the left and right hand
    5.62 -sides; attributes are applied to any immediately preceding theorem.  If names
    5.63 -are omitted, the theorems are not stored within the theorem database of the
    5.64 -theory or proof context; any given attributes are still applied, though.
    5.65 +sides; attributes are applied to any immediately preceding fact.  If names are
    5.66 +omitted, the theorems are not stored within the theorem database of the theory
    5.67 +or proof context; any given attributes are still applied, though.
    5.68  
    5.69  \indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
    5.70  \indexouternonterm{thmdef}\indexouternonterm{thmrefs}
    5.71 @@ -365,9 +365,9 @@
    5.72  
    5.73  Wherever explicit propositions (or term fragments) occur in a proof text,
    5.74  casual binding of schematic term variables may be given specified via patterns
    5.75 -of the form $\ISS{p@1\;\dots}{p@n}$.  There are separate versions available
    5.76 -for \railqtoken{term}s and \railqtoken{prop}s.  The latter provides a
    5.77 -$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    5.78 +of the form ``$\ISS{p@1\;\dots}{p@n}$''.  There are separate versions
    5.79 +available for \railqtoken{term}s and \railqtoken{prop}s.  The latter provides
    5.80 +a $\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    5.81  
    5.82  \indexouternonterm{termpat}\indexouternonterm{proppat}
    5.83  \begin{rail}
    5.84 @@ -380,8 +380,8 @@
    5.85  Declarations of local variables $x :: \tau$ and logical propositions $a :
    5.86  \phi$ represent different views on the same principle of introducing a local
    5.87  scope.  In practice, one may usually omit the typing of $vars$ (due to
    5.88 -type-inference), and the naming of propositions (due to implicit chaining of
    5.89 -emerging facts).  In any case, Isar proof elements usually admit to introduce
    5.90 +type-inference), and the naming of propositions (due to implicit references of
    5.91 +current facts).  In any case, Isar proof elements usually admit to introduce
    5.92  multiple such items simultaneously.
    5.93  
    5.94  \indexouternonterm{vars}\indexouternonterm{props}
    5.95 @@ -419,8 +419,8 @@
    5.96  preparation system (see also \S\ref{sec:document-prep}).
    5.97  
    5.98  Thus embedding of
    5.99 -\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
   5.100 -text block would cause
   5.101 +``\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}''
   5.102 +within a text block would cause
   5.103  \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
   5.104  to appear in the final {\LaTeX} document.  Also note that theorem
   5.105  antiquotations may involve attributes as well.  For example,
   5.106 @@ -453,25 +453,32 @@
   5.107  \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
   5.108  
   5.109  \begin{descr}
   5.110 +  
   5.111  \item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
   5.112    specifications may be included as well (see also \S\ref{sec:syn-att}); the
   5.113    $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
   5.114    useful to suppress printing of schematic variables.
   5.115 +
   5.116  \item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
   5.117 +
   5.118  \item [$\at\{term~t\}$] prints a well-typed term $t$.
   5.119 +
   5.120  \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
   5.121 +  
   5.122  \item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
   5.123    particularly useful to print portions of text according to the Isabelle
   5.124    {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
   5.125 -  of terms that cannot be parsed or type-checked yet).
   5.126 +  of terms that should not be parsed or type-checked yet).
   5.127 +  
   5.128  \item [$\at\{goals\}$] prints the current \emph{dynamic} goal state.  This is
   5.129 -  only for support of tactic-emulation scripts within Isar --- presentation of
   5.130 -  goal states does not conform to actual human-readable proof documents.
   5.131 -  
   5.132 +  mainly for support of tactic-emulation scripts within Isar --- presentation
   5.133 +  of goal states does not conform to actual human-readable proof documents.
   5.134    Please do not include goal states into document output unless you really
   5.135    know what you are doing!
   5.136 +
   5.137  \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
   5.138    print the main goal.
   5.139 +
   5.140  \end{descr}
   5.141  
   5.142  \medskip
   5.143 @@ -507,9 +514,10 @@
   5.144  the above flags are disabled by default, unless changed from ML.
   5.145  
   5.146  \medskip Note that antiquotations do not only spare the author from tedious
   5.147 -typing, but also achieve some degree of consistency-checking of informal
   5.148 -explanations with formal developments, since well-formedness of terms and
   5.149 -types with respect to the current theory or proof context can be ensured.
   5.150 +typing of logical entities, but also achieve some degree of
   5.151 +consistency-checking of informal explanations with formal developments:
   5.152 +well-formedness of terms and types with respect to the current theory or proof
   5.153 +context is ensured here.
   5.154  
   5.155  %%% Local Variables: 
   5.156  %%% mode: latex