\begin{isabelle}%
\isacommand{theory}~NatClass~=~FOL:\isanewline
\isanewline
\isacommand{consts}\isanewline
~~zero~::~'a~~~~({"}0{"})\isanewline
~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
~~rec~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~'a{"}\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~nat~<~{"}term{"}\isanewline
~~induct:~~~~~{"}P(0)~{\isasymLongrightarrow}~({\isasymAnd}x.~P(x)~{\isasymLongrightarrow}~P(Suc(x)))~{\isasymLongrightarrow}~P(n){"}\isanewline
~~Suc\_inject:~{"}Suc(m)~=~Suc(n)~{\isasymLongrightarrow}~m~=~n{"}\isanewline
~~Suc\_neq\_0:~~{"}Suc(m)~=~0~{\isasymLongrightarrow}~R{"}\isanewline
~~rec\_0:~~~~~~{"}rec(0,~a,~f)~=~a{"}\isanewline
~~rec\_Suc:~~~~{"}rec(Suc(m),~a,~f)~=~f(m,~rec(m,~a,~f)){"}\isanewline
\isanewline
\isacommand{constdefs}\isanewline
~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline
~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}\isanewline
\isanewline
\isacommand{end}\end{isabelle}%