doc-src/IsarRef/basics.tex
changeset 7466 7df66ce6508a
parent 7335 abba35b98892
child 7895 7c492d8bc8e3
     1.1 --- a/doc-src/IsarRef/basics.tex	Sat Sep 04 20:55:52 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Sat Sep 04 20:57:32 1999 +0200
     1.3 @@ -3,8 +3,9 @@
     1.4  
     1.5  Isabelle/Isar offers two main improvements over classic Isabelle:
     1.6  \begin{enumerate}
     1.7 -\item A new \emph{theory format}, often referred to as ``new-style theories'',
     1.8 -  supporting interactive development and unlimited undo operation.
     1.9 +\item A new \emph{theory format}, occasionally referred to as ``new-style
    1.10 +  theories'', supporting interactive development with unlimited undo
    1.11 +  operation.
    1.12  \item A \emph{formal proof language} designed to support intelligible
    1.13    semi-automated reasoning.  Rather than putting together tactic scripts, the
    1.14    author is enabled to express the reasoning in way that is close to
    1.15 @@ -13,32 +14,35 @@
    1.16  
    1.17  The Isar proof language is embedded into the new theory format as a proper
    1.18  sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    1.19 -$\LEMMANAME$ at the theory level, and left with the final end of proof (e.g.\ 
    1.20 -via $\QEDNAME$).  Some theory extension mechanisms require proof as well, such
    1.21 -as the HOL $\isarkeyword{typedef}$ which only works for non-empty representing
    1.22 -sets.
    1.23 +$\LEMMANAME$ at the theory level, and left with the conclusion of the proof
    1.24 +(via $\QEDNAME$ etc.).  Some theory extension mechanisms require proof as
    1.25 +well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
    1.26 +the representing sets.
    1.27  
    1.28  New-style theory files may still be associated with an ML file consisting of
    1.29  plain old tactic scripts.  There is no longer any ML binding generated for the
    1.30 -theory and theorems, though.  Functions \texttt{theory}, \texttt{thm}, and
    1.31 -\texttt{thms} may be used to retrieve this information from ML
    1.32 -\cite{isabelle-ref}.  Nevertheless, migration between classic Isabelle and
    1.33 -Isabelle/Isar is relatively easy.  Thus users may start to benefit from
    1.34 -interactive theory development even before they have any idea of the Isar
    1.35 -proof language.
    1.36 +theory and theorems, though.  ML functions \texttt{theory}, \texttt{thm}, and
    1.37 +\texttt{thms} retrieve this information \cite{isabelle-ref}.  Nevertheless,
    1.38 +migration between classic Isabelle and Isabelle/Isar is relatively easy.  Thus
    1.39 +users may start to benefit from interactive theory development even before
    1.40 +they have any idea of the Isar proof language.
    1.41  
    1.42  \begin{warn}
    1.43 -  Proof~General does \emph{not} support mixed interactive development of
    1.44 -  classic Isabelle theory files and tactic scripts together with Isar
    1.45 -  documents at the same time.  The ``\texttt{isa}'' and ``\texttt{isar}''
    1.46 -  versions of Proof~General are handled as two different theorem proving
    1.47 -  systems, only one may be active at the same time.
    1.48 +  Currently Proof~General does \emph{not} support mixed interactive
    1.49 +  development of classic Isabelle theory files and tactic scripts together
    1.50 +  with Isar documents at the same time.  The ``\texttt{isa}'' and
    1.51 +  ``\texttt{isar}'' versions of Proof~General are handled as two different
    1.52 +  theorem proving systems, only one may be active at the same time.
    1.53  \end{warn}
    1.54  
    1.55 +Porting of existing tactic scripts is best done by running two separate
    1.56 +Proof~General sessions, one for replaying the old script and the other for the
    1.57 +emerging Isabelle/Isar document.
    1.58 +
    1.59  
    1.60  \section{The Isar proof language}
    1.61  
    1.62 -Sorry, this rather important section has not been written yet!  Refer to
    1.63 +Sorry, this important section has not been written yet!  Refer to
    1.64  \cite{Wenzel:1999:TPHOL} for the time being.
    1.65  
    1.66  \subsection{Commands}