--- a/doc-src/IsarRef/basics.tex Sat Oct 30 20:12:23 1999 +0200
+++ b/doc-src/IsarRef/basics.tex Sat Oct 30 20:13:16 1999 +0200
@@ -1,61 +1,7 @@
-\chapter{Basic Concepts}\label{ch:basics}
-
-\section{Isabelle/Isar theories}
-
-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 and unlimited undo operation.
-\item A \emph{formal proof document language} designed to support intelligible
- semi-automated reasoning. Instead of putting together unreadable 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 again with the final conclusion
-(e.g.\ via $\QEDNAME$). A few 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 of these may be active.
-\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}
+%FIXME
+%\chapter{Basic Concepts}\label{ch:basics}
+%\section{The Isar proof language}
%%% Local Variables:
%%% mode: latex