src/HOL/Extraction/Pigeonhole.thy
changeset 17027 8bbe57116d13
parent 17024 ae4a8446df16
child 17145 e623e57b0f44
--- 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"}.
 *}