Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tuned comment.
authorberghofe
Sat, 06 Aug 2005 18:06:56 +0200
changeset 17027 8bbe57116d13
parent 17026 43cc86fd3536
child 17028 a497f621bfd4
Tuned comment.
src/HOL/Extraction/Pigeonhole.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction/Pigeonhole.thy	Sat Aug 06 08:16:19 2005 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Sat Aug 06 18:06:56 2005 +0200
@@ -24,7 +24,7 @@
   done
 
 text {*
-We can decide whether an array @{term "f"} of length @{term "l+(1::nat)"}
+We can decide whether an array @{term "f"} of length @{term "l"}
 contains an element @{term "x"}.
 *}
isabelle