src/HOL/Hoare/Examples.ML
changeset 11464 ddea204de5bc
parent 10962 cda180b1e2e0
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Hoare/Examples.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  Ambiguity warnings of parser are due to := being used
     1.5  both for assignment and list update.
     1.6  *)
     1.7 -Goal "m - 1 < n ==> m < Suc n";
     1.8 +Goal "m - 1' < n ==> m < Suc n";
     1.9  by (arith_tac 1);
    1.10  qed "lemma";
    1.11  
    1.12 @@ -184,7 +184,7 @@
    1.13  \   geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
    1.14  \ |- VARS A u l.\
    1.15  \ {0 < length(A::('a::order)list)} \
    1.16 -\ l := 0; u := length A - 1; \
    1.17 +\ l := 0; u := length A - 1'; \
    1.18  \ WHILE l <= u \
    1.19  \  INV {leq A l & geq A u & u<length A & l<=length A} \
    1.20  \  DO WHILE l < length A & A!l <= pivot \