| changeset 48994 | c84278efa9d5 |
| parent 48985 | 5386df44a037 |
| child 58860 | fee7cfa69c50 |
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy Wed Aug 29 12:07:45 2012 +0200 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Wed Aug 29 12:07:57 2012 +0200 @@ -132,8 +132,8 @@ function: *}; -consts f :: "nat \<Rightarrow> nat"; -axioms f_ax: "f(f(n)) < f(Suc(n))"; +axiomatization f :: "nat \<Rightarrow> nat" + where f_ax: "f(f(n)) < f(Suc(n))" text{* \begin{warn}