| changeset 10971 | 6852682eaf16 |
| parent 10885 | 90695f46440b |
| child 10978 | 5eebea8f359f |
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 11:59:15 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 12:29:10 2001 +0100 @@ -55,7 +55,7 @@ datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex; text{*\noindent -The evaluation if If-expressions proceeds as for @{typ"boolex"}: +The evaluation of If-expressions proceeds as for @{typ"boolex"}: *} consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";