# HG changeset patch
# User nipkow
# Date 1024490290 -7200
# Node ID aea757ff88ce768a46876b2080bd4d825053c105
# Parent  b6fc6e4a0a24296a304a07dde707a3a823612d83
0 -> key

diff -r b6fc6e4a0a24 -r aea757ff88ce src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Wed Jun 19 12:48:55 2002 +0200
+++ b/src/HOL/Hoare/Examples.ML	Wed Jun 19 14:38:10 2002 +0200
@@ -150,16 +150,16 @@
 
 (*** ARRAYS ***)
 
-(* Search for 0 *)
+(* Search for a key *)
 Goal
 "|- VARS A i. \
 \ {True} \
 \ i := 0; \
-\ WHILE i < length A & A!i ~= 0 \
-\ INV {!j. j<i --> A!j ~= 0} \
+\ WHILE i < length A & A!i ~= key \
+\ INV {!j. j<i --> A!j ~= key} \
 \ DO i := i+1 OD \
-\ {(i < length A --> A!i = 0) & \
-\  (i = length A --> (!j. j < length A --> A!j ~= 0))}";
+\ {(i < length A --> A!i = key) & \
+\  (i = length A --> (!j. j < length A --> A!j ~= key))}";
 by (hoare_tac Asm_full_simp_tac 1);
 by (blast_tac (claset() addSEs [less_SucE]) 1);
 qed "zero_search";