changeset 11457 | 279da0358aa9 |
parent 11456 | 7eb63f63e6c6 |
child 12699 | deae80045527 |
--- a/doc-src/TutorialI/Misc/case_exprs.thy Thu Jul 26 16:43:02 2001 +0200 +++ b/doc-src/TutorialI/Misc/case_exprs.thy Thu Jul 26 18:23:38 2001 +0200 @@ -68,7 +68,6 @@ simplification, so no special methods are provided for them. \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