doc-src/IsarRef/basics.tex
changeset 7315 76a39a3784b5
parent 7297 c1eeeadbe80a
child 7335 abba35b98892
     1.1 --- a/doc-src/IsarRef/basics.tex	Sun Aug 22 18:21:36 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Sun Aug 22 21:13:20 1999 +0200
     1.3 @@ -4,23 +4,36 @@
     1.4  Isabelle/Isar offers two main improvements over classic Isabelle:
     1.5  \begin{enumerate}
     1.6  \item A new \emph{theory format}, often referred to as ``new-style theories'',
     1.7 -  supporting interactive development with unlimited undo operation.
     1.8 -\item A formal \emph{proof language} language designed to support
     1.9 -  \emph{intelligible} semi-automated reasoning.  Rather than putting together
    1.10 -  tactic scripts, the author is enabled to express the reasoning in way that
    1.11 -  is close to mathematical practice.
    1.12 +  supporting interactive development and unlimited undo operation.
    1.13 +\item A \emph{formal proof language} designed to support intelligible
    1.14 +  semi-automated reasoning.  Rather than putting together tactic scripts, the
    1.15 +  author is enabled to express the reasoning in way that is close to
    1.16 +  mathematical practice.
    1.17  \end{enumerate}
    1.18  
    1.19  The Isar proof language is embedded into the new theory format as a proper
    1.20  sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    1.21 -$\LEMMANAME$ at the theory levels, and left with the final end of proof.  Some
    1.22 -theory extension mechanisms require proof as well, such as the HOL
    1.23 -$\isarkeyword{typedef}$.
    1.24 +$\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\ 
    1.25 +via $\QEDNAME$).  Some theory extension mechanisms require proof as well, such
    1.26 +as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty
    1.27 +representing sets.
    1.28  
    1.29  New-style theory files may still be associated with an ML file consisting of
    1.30 -plain old tactic scripts.  Generally, migration between the two formats is
    1.31 -made relatively easy, and users may start to benefit from interactive theory
    1.32 -development even before they have any idea of the Isar proof language.
    1.33 +plain old tactic scripts.  There is no longer any ML binding generated for the
    1.34 +theory and theorems, though.  Functions \texttt{theory}, \texttt{thm}, and
    1.35 +\texttt{thms} may be used to retrieve this information from ML (see also
    1.36 +\cite{isabelle-ref}).  Nevertheless, migration between classic Isabelle and
    1.37 +Isabelle/Isar is relatively easy.  Thus users may start to benefit from
    1.38 +interactive theory development even before they have any idea of the Isar
    1.39 +proof language.
    1.40 +
    1.41 +\begin{warn}
    1.42 +  Proof~General does \emph{not} support mixed interactive development of
    1.43 +  classic Isabelle theory files and tactic scripts together with Isar
    1.44 +  documents at the same time.  The \texttt{isa} and \texttt{isar} versions of
    1.45 +  Proof~General appear as two different theorem proving systems; only one
    1.46 +  prover may be active at any time.
    1.47 +\end{warn}
    1.48  
    1.49  
    1.50  \section{The Isar proof language}