| changeset 28752 | 754f10154d73 |
| parent 28687 | 150a8a1eae1a |
| child 28760 | cbc435f7b16b |
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:33:56 2008 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:34:23 2008 +0100 @@ -859,7 +859,7 @@ *} -section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *} +section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *} text {* The following tools of Isabelle/HOL support cases analysis and