--- a/doc-src/TutorialI/fp.tex Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Jan 08 10:33:51 2001 +0100
@@ -219,15 +219,6 @@
\input{Misc/document/case_exprs.tex}
-\begin{warn}
- Induction is only allowed on free (or \isasymAnd-bound) variables that
- should not occur among the assumptions of the subgoal; see
- {\S}\ref{sec:ind-var-in-prems} for details. Case distinction
- (\isa{case_tac}) works for arbitrary terms, which need to be
- quoted if they are non-atomic.
-\end{warn}
-
-
\input{Ifexpr/document/Ifexpr.tex}
\section{Some basic types}