generate 'code' attribute only if 'code' plugin is enabled
(*<*)theory fakenat imports Main begin;(*>*)text{*\noindentThe type \tydx{nat} of naturalnumbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.It behaves approximately as if it were declared like this:*}datatype nat = zero ("0") | Suc nat(*<*)end(*>*)