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

author | nipkow |

Mon, 11 Jul 2005 19:59:11 +0200 | |

changeset 16768 | 37636be4cbd1 |

parent 16767 | 2d4433759b8d |

child 16769 | 7f188f2127f7 |

small text mod

--- a/doc-src/TutorialI/Misc/natsum.thy Mon Jul 11 16:42:42 2005 +0200 +++ b/doc-src/TutorialI/Misc/natsum.thy Mon Jul 11 19:59:11 2005 +0200 @@ -80,7 +80,7 @@ text{*\noindent For efficiency's sake, this built-in prover ignores quantified formulae, -logical connectives, and all arithmetic operations apart from addition. +many logical connectives, and all arithmetic operations apart from addition. In consequence, @{text auto} and @{text simp} cannot prove this slightly more complex goal: *} @@ -119,7 +119,7 @@ @{text k}~\sdx{dvd} are also supported, where the former two are eliminated by case distinctions, again blowing up the running time. -If the formula involves explicit quantifiers, @{text arith} may take +If the formula involves quantifiers, @{text arith} may take super-exponential time and space. \end{warn} *}