diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/fp.tex --- 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}