diff -r fce25292e1b8 -r 5120a2a15d06 doc-src/IsarRef/basics.tex
--- 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