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