1.1 --- a/src/HOL/Hoare/Examples.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -50,9 +50,9 @@
     1.4  Goal "|- VARS a b x y. \
     1.5  \ {0<A & 0<B & a=A & b=B & x=B & y=A} \
     1.6  \ WHILE  a ~= b  \
     1.7 -\ INV {0<a & 0<b & gcd A B = gcd a b & # 2*A*B = a*x + b*y} \
     1.8 +\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \
     1.9  \ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
    1.10 -\ {a = gcd A B & # 2*A*B = a*(x+y)}";
    1.11 +\ {a = gcd A B & 2*A*B = a*(x+y)}";
    1.12  by (hoare_tac (K all_tac) 1);
    1.13  by(Asm_simp_tac 1);
    1.14  by(asm_simp_tac (simpset() addsimps
    1.15 @@ -68,9 +68,9 @@
    1.16  \ c := (1::nat); \
    1.17  \ WHILE b ~= 0 \
    1.18  \ INV {A^B = c * a^b} \
    1.19 -\ DO  WHILE b mod # 2 = 0 \
    1.20 +\ DO  WHILE b mod 2 = 0 \
    1.21  \     INV {A^B = c * a^b} \
    1.22 -\     DO  a := a*a; b := b div # 2 OD; \
    1.23 +\     DO  a := a*a; b := b div 2 OD; \
    1.24  \     c := c*a; b := b - 1 \
    1.25  \ OD \
    1.26  \ {c = A^B}";
    1.27 @@ -114,7 +114,7 @@
    1.28  \ x := X; u := 1; w := 1; r := (0::nat); \
    1.29  \ WHILE w <= x \
    1.30  \ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
    1.31 -\ DO r := r + 1; w := w + u + # 2; u := u + # 2 OD \
    1.32 +\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \
    1.33  \ {r*r <= X & X < (r+1)*(r+1)}";
    1.34  by (hoare_tac (SELECT_GOAL Auto_tac) 1);
    1.35  qed "sqrt_without_multiplication";