| changeset 63178 | b9e1d53124f5 |
| parent 58860 | fee7cfa69c50 |
| child 67406 | 23307fd33906 |
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy Sat May 28 17:35:12 2016 +0200 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy Sat May 28 21:38:58 2016 +0200 @@ -133,7 +133,7 @@ *} axiomatization f :: "nat \<Rightarrow> nat" - where f_ax: "f(f(n)) < f(Suc(n))" + where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat text{* \begin{warn}