doc-src/IsarRef/basics.tex
changeset 7981 5120a2a15d06
parent 7895 7c492d8bc8e3
     1.1 --- a/doc-src/IsarRef/basics.tex	Sat Oct 30 20:12:23 1999 +0200
     1.2 +++ b/doc-src/IsarRef/basics.tex	Sat Oct 30 20:13:16 1999 +0200
     1.3 @@ -1,61 +1,7 @@
     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 and unlimited undo operation.
    1.13 -\item A \emph{formal proof document language} designed to support intelligible
    1.14 -  semi-automated reasoning.  Instead of putting together unreadable tactic
    1.15 -  scripts, the author is enabled to express the reasoning in way that is close
    1.16 -  to mathematical practice.
    1.17 -\end{enumerate}
    1.18 -
    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 level, and left again with the final conclusion
    1.22 -(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
    1.23 -well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
    1.24 -the representing sets.
    1.25 -
    1.26 -New-style theory files may still be associated with an ML file consisting of
    1.27 -plain old tactic scripts.  There is no longer any ML binding generated for the
    1.28 -theory and theorems, though.  ML functions \texttt{theory}, \texttt{thm}, and
    1.29 -\texttt{thms} retrieve this information \cite{isabelle-ref}.  Nevertheless,
    1.30 -migration between classic Isabelle and Isabelle/Isar is relatively easy.  Thus
    1.31 -users may start to benefit from interactive theory development even before
    1.32 -they have any idea of the Isar proof language.
    1.33 -
    1.34 -\begin{warn}
    1.35 -  Currently Proof~General does \emph{not} support mixed interactive
    1.36 -  development of classic Isabelle theory files and tactic scripts, together
    1.37 -  with Isar documents at the same time.  The ``\texttt{isa}'' and
    1.38 -  ``\texttt{isar}'' versions of Proof~General are handled as two different
    1.39 -  theorem proving systems, only one of these may be active.
    1.40 -\end{warn}
    1.41 -
    1.42 -Porting of existing tactic scripts is best done by running two separate
    1.43 -Proof~General sessions, one for replaying the old script and the other for the
    1.44 -emerging Isabelle/Isar document.
    1.45 -
    1.46 -
    1.47 -\section{The Isar proof language}
    1.48 -
    1.49 -Sorry, this important section has not been written yet!  Refer to
    1.50 -\cite{Wenzel:1999:TPHOL} for the time being.
    1.51 -
    1.52 -\subsection{Commands}
    1.53 -
    1.54 -\subsubsection{Isar primitives}
    1.55 -
    1.56 -\subsubsection{Derived elements}
    1.57 -
    1.58 -
    1.59 -\subsection{Methods}
    1.60 -
    1.61 -\subsection{Attributes}
    1.62 +%FIXME
    1.63 +%\chapter{Basic Concepts}\label{ch:basics}
    1.64 +%\section{The Isar proof language}
    1.65  
    1.66  %%% Local Variables: 
    1.67  %%% mode: latex