doc-src/IsarRef/basics.tex
changeset 7895 7c492d8bc8e3
parent 7466 7df66ce6508a
child 7981 5120a2a15d06
     1.1 --- a/doc-src/IsarRef/basics.tex	Thu Oct 21 15:57:26 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Thu Oct 21 17:42:21 1999 +0200
     1.3 @@ -1,21 +1,22 @@
     1.4  
     1.5  \chapter{Basic Concepts}\label{ch:basics}
     1.6  
     1.7 +\section{Isabelle/Isar theories}
     1.8 +
     1.9  Isabelle/Isar offers two main improvements over classic Isabelle:
    1.10  \begin{enumerate}
    1.11  \item A new \emph{theory format}, occasionally referred to as ``new-style
    1.12 -  theories'', supporting interactive development with unlimited undo
    1.13 -  operation.
    1.14 -\item A \emph{formal proof language} designed to support intelligible
    1.15 -  semi-automated reasoning.  Rather than putting together tactic scripts, the
    1.16 -  author is enabled to express the reasoning in way that is close to
    1.17 -  mathematical practice.
    1.18 +  theories'', supporting interactive development and unlimited undo operation.
    1.19 +\item A \emph{formal proof document language} designed to support intelligible
    1.20 +  semi-automated reasoning.  Instead of putting together unreadable tactic
    1.21 +  scripts, the author is enabled to express the reasoning in way that is close
    1.22 +  to mathematical practice.
    1.23  \end{enumerate}
    1.24  
    1.25  The Isar proof language is embedded into the new theory format as a proper
    1.26  sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    1.27 -$\LEMMANAME$ at the theory level, and left with the conclusion of the proof
    1.28 -(via $\QEDNAME$ etc.).  Some theory extension mechanisms require proof as
    1.29 +$\LEMMANAME$ at the theory level, and left again with the final conclusion
    1.30 +(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
    1.31  well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
    1.32  the representing sets.
    1.33  
    1.34 @@ -29,10 +30,10 @@
    1.35  
    1.36  \begin{warn}
    1.37    Currently Proof~General does \emph{not} support mixed interactive
    1.38 -  development of classic Isabelle theory files and tactic scripts together
    1.39 +  development of classic Isabelle theory files and tactic scripts, together
    1.40    with Isar documents at the same time.  The ``\texttt{isa}'' and
    1.41    ``\texttt{isar}'' versions of Proof~General are handled as two different
    1.42 -  theorem proving systems, only one may be active at the same time.
    1.43 +  theorem proving systems, only one of these may be active.
    1.44  \end{warn}
    1.45  
    1.46  Porting of existing tactic scripts is best done by running two separate
    1.47 @@ -56,7 +57,6 @@
    1.48  
    1.49  \subsection{Attributes}
    1.50  
    1.51 -
    1.52  %%% Local Variables: 
    1.53  %%% mode: latex
    1.54  %%% TeX-master: "isar-ref"