summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/IsarRef/hol.tex

changeset 9751 | 1287787744a7 |

parent 9695 | ec7d7f877712 |

child 9800 | 221388d5696d |

equal
deleted
inserted
replaced

9750:270cd9831e7b | 9751:1287787744a7 |
---|---|

144 datatypes. |
144 datatypes. |

145 \item [$\isarkeyword{recdef}$] defines general well-founded recursive |
145 \item [$\isarkeyword{recdef}$] defines general well-founded recursive |

146 functions (using the TFL package). |
146 functions (using the TFL package). |

147 \end{descr} |
147 \end{descr} |

148 |
148 |

149 Both definitions accommodate reasoning proof by induction (cf.\ |
149 Both definitions accommodate reasoning by induction (cf.\ |

150 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name |
150 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name |

151 of the function definition) refers to a specific induction rule, with |
151 of the function definition) refers to a specific induction rule, with |

152 parameters named according to the user-specified equations. Case names of |
152 parameters named according to the user-specified equations. Case names of |

153 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
153 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of |

154 $\isarkeyword{recdef}$ are numbered (starting from $1$). |
154 $\isarkeyword{recdef}$ are numbered (starting from $1$). |