| changeset 10884 | 2995639c6a09 |
| parent 10790 | 520dd8696927 |
| child 11494 | 23a118849801 |
--- a/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 12 16:19:44 2001 +0100 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 12 16:28:14 2001 +0100 @@ -1,6 +1,6 @@ (*<*)theory Mutual = Main:(*>*) -subsection{*Mutually inductive definitions*} +subsection{*Mutually Inductive Definitions*} text{* Just as there are datatypes defined by mutual recursion, there are sets defined