renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
(*<*)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 as if it were declared like this:*}datatype nat = 0 | Suc nat(*<*)end(*>*)