# HG changeset patch
# User berghofe
# Date 1123344416 -7200
# Node ID 8bbe57116d13f7daf5330fd4b2bfa1ae1c8e5d5e
# Parent  43cc86fd35369688b23efd1d97e7400660b78bd2
Tuned comment.

diff -r 43cc86fd3536 -r 8bbe57116d13 src/HOL/Extraction/Pigeonhole.thy
--- 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"}.
 *}