doc-src/TutorialI/Misc/case_exprs.thy
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