doc-src/IsarRef/basics.tex

updated;

\chapter{Basic Concepts}\label{ch:basics}

Isabelle/Isar offers two main improvements over classic Isabelle:
\begin{enumerate}
\item A new \emph{theory format}, occasionally referred to as ``new-style
  theories'', supporting interactive development with unlimited undo
  operation.
\item A \emph{formal proof language} designed to support intelligible
  semi-automated reasoning.  Rather than putting together tactic scripts, the
  author is enabled to express the reasoning in way that is close to
  mathematical practice.
\end{enumerate}

The Isar proof language is embedded into the new theory format as a proper
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
$\LEMMANAME$ at the theory level, and left with the conclusion of the proof
(via $\QEDNAME$ etc.).  Some theory extension mechanisms require proof as
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
the representing sets.

New-style theory files may still be associated with an ML file consisting of
plain old tactic scripts.  There is no longer any ML binding generated for the
theory and theorems, though.  ML functions \texttt{theory}, \texttt{thm}, and
\texttt{thms} retrieve this information \cite{isabelle-ref}.  Nevertheless,
migration between classic Isabelle and Isabelle/Isar is relatively easy.  Thus
users may start to benefit from interactive theory development even before
they have any idea of the Isar proof language.

\begin{warn}
  Currently Proof~General does \emph{not} support mixed interactive
  development of classic Isabelle theory files and tactic scripts together
  with Isar documents at the same time.  The ``\texttt{isa}'' and
  ``\texttt{isar}'' versions of Proof~General are handled as two different
  theorem proving systems, only one may be active at the same time.
\end{warn}

Porting of existing tactic scripts is best done by running two separate
Proof~General sessions, one for replaying the old script and the other for the
emerging Isabelle/Isar document.


\section{The Isar proof language}

Sorry, this important section has not been written yet!  Refer to
\cite{Wenzel:1999:TPHOL} for the time being.

\subsection{Commands}

\subsubsection{Isar primitives}

\subsubsection{Derived elements}


\subsection{Methods}

\subsection{Attributes}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: