summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Wed, 14 Apr 2010 19:46:36 +0200 | |

changeset 36139 | 0c2538afe8e8 |

parent 36138 | 1faa0fc34174 |

child 36144 | e8db171b8643 |

Spelling error: theroems -> theorems

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 17:50:22 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 19:46:36 2010 +0200 @@ -471,7 +471,7 @@ Note that the resulting simplification and induction rules correspond to the transformed specification, not the one given originally. This usually means that each equation given by the user - may result in several theroems. Also note that this automatic + may result in several theorems. Also note that this automatic transformation only works for ML-style datatype patterns. \item @{text domintros} enables the automated generation of

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 14 17:50:22 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 14 19:46:36 2010 +0200 @@ -479,7 +479,7 @@ Note that the resulting simplification and induction rules correspond to the transformed specification, not the one given originally. This usually means that each equation given by the user - may result in several theroems. Also note that this automatic + may result in several theorems. Also note that this automatic transformation only works for ML-style datatype patterns. \item \isa{domintros} enables the automated generation of