Paper/Paper.thy
changeset 164 8a3e63163910
parent 162 a63c3f8d7234
child 169 6013ca0e6e22
equal deleted inserted replaced
163:67063c5365e1 164:8a3e63163910
  1294   \emph{Recursive functions} are defined as the datatype
  1294   \emph{Recursive functions} are defined as the datatype
  1295 
  1295 
  1296   \begin{center}
  1296   \begin{center}
  1297   \begin{tabular}{c@ {\hspace{4mm}}c}
  1297   \begin{tabular}{c@ {\hspace{4mm}}c}
  1298   \begin{tabular}{rcl@ {\hspace{4mm}}l}
  1298   \begin{tabular}{rcl@ {\hspace{4mm}}l}
  1299   @{term r} & @{text "::="} & @{term z} & (zero-functions)\\
  1299   @{term r} & @{text "::="} & @{term z} & (zero-function)\\
  1300             & @{text "|"}   & @{term s} & (successor-function)\\
  1300             & @{text "|"}   & @{term s} & (successor-function)\\
  1301             & @{text "|"}   & @{term "id n m"} & (projection)\\
  1301             & @{text "|"}   & @{term "id n m"} & (projection)\\
  1302   \end{tabular} &
  1302   \end{tabular} &
  1303   \begin{tabular}{cl@ {\hspace{4mm}}l}
  1303   \begin{tabular}{cl@ {\hspace{4mm}}l}
  1304   @{text "|"} & @{term "Cn n r rs"} & (composition)\\
  1304   @{text "|"} & @{term "Cn n r rs"} & (composition)\\