doc-src/IsarRef/basics.tex
author wenzelm
Thu Aug 19 20:05:13 1999 +0200 (1999-08-19)
changeset 7297 c1eeeadbe80a
parent 7135 8eabfd7e6b9b
child 7315 76a39a3784b5
permissions -rw-r--r--
more;
     1 
     2 \chapter{Basic Concepts}\label{ch:basics}
     3 
     4 Isabelle/Isar offers two main improvements over classic Isabelle:
     5 \begin{enumerate}
     6 \item A new \emph{theory format}, often referred to as ``new-style theories'',
     7   supporting interactive development with unlimited undo operation.
     8 \item A formal \emph{proof language} language designed to support
     9   \emph{intelligible} semi-automated reasoning.  Rather than putting together
    10   tactic scripts, the author is enabled to express the reasoning in way that
    11   is close to mathematical practice.
    12 \end{enumerate}
    13 
    14 The Isar proof language is embedded into the new theory format as a proper
    15 sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
    16 $\LEMMANAME$ at the theory levels, and left with the final end of proof.  Some
    17 theory extension mechanisms require proof as well, such as the HOL
    18 $\isarkeyword{typedef}$.
    19 
    20 New-style theory files may still be associated with an ML file consisting of
    21 plain old tactic scripts.  Generally, migration between the two formats is
    22 made relatively easy, and users may start to benefit from interactive theory
    23 development even before they have any idea of the Isar proof language.
    24 
    25 
    26 \section{The Isar proof language}
    27 
    28 This rather important section has not been written yet!  Refer to
    29 \cite{Wenzel:1999:TPHOL} for the time being.
    30 
    31 \subsection{Commands}
    32 
    33 \subsubsection{Isar primitives}
    34 
    35 \subsubsection{Derived elements}
    36 
    37 
    38 \subsection{Methods}
    39 
    40 \subsection{Attributes}
    41 
    42 
    43 %%% Local Variables: 
    44 %%% mode: latex
    45 %%% TeX-master: "isar-ref"
    46 %%% End: