doc-src/IsarRef/basics.tex
changeset 7297 c1eeeadbe80a
parent 7135 8eabfd7e6b9b
child 7315 76a39a3784b5
     1.1 --- a/doc-src/IsarRef/basics.tex	Thu Aug 19 19:56:17 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Thu Aug 19 20:05:13 1999 +0200
     1.3 @@ -1,11 +1,39 @@
     1.4  
     1.5 -\chapter{Basic Concepts}
     1.6 +\chapter{Basic Concepts}\label{ch:basics}
     1.7 +
     1.8 +Isabelle/Isar offers two main improvements over classic Isabelle:
     1.9 +\begin{enumerate}
    1.10 +\item A new \emph{theory format}, often referred to as ``new-style theories'',
    1.11 +  supporting interactive development with unlimited undo operation.
    1.12 +\item A formal \emph{proof language} language designed to support
    1.13 +  \emph{intelligible} semi-automated reasoning.  Rather than putting together
    1.14 +  tactic scripts, the author is enabled to express the reasoning in way that
    1.15 +  is close to mathematical practice.
    1.16 +\end{enumerate}
    1.17  
    1.18 -\section{Isabelle/Isar Theories}
    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 +
    1.25 +New-style theory files may still be associated with an ML file consisting of
    1.26 +plain old tactic scripts.  Generally, migration between the two formats is
    1.27 +made relatively easy, and users may start to benefit from interactive theory
    1.28 +development even before they have any idea of the Isar proof language.
    1.29 +
    1.30  
    1.31  \section{The Isar proof language}
    1.32  
    1.33 -\subsection{Proof commands}
    1.34 +This rather important section has not been written yet!  Refer to
    1.35 +\cite{Wenzel:1999:TPHOL} for the time being.
    1.36 +
    1.37 +\subsection{Commands}
    1.38 +
    1.39 +\subsubsection{Isar primitives}
    1.40 +
    1.41 +\subsubsection{Derived elements}
    1.42 +
    1.43  
    1.44  \subsection{Methods}
    1.45