src/HOL/Hoare/Examples.thy
changeset 13857 11d7c5a8dbb7
parent 13789 d37f66755f47
child 15197 19e735596e51
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Mar 11 15:04:24 2003 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Mar 11 15:04:24 2003 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  lemma Euclid_GCD: "VARS a b
     1.5   {0<A & 0<B}
     1.6   a := A; b := B;
     1.7 - WHILE  a~=b
     1.8 + WHILE  a \<noteq> b
     1.9   INV {0<a & 0<b & gcd A B = gcd a b}
    1.10   DO IF a<b THEN b := b-a ELSE a := a-b FI OD
    1.11   {a = gcd A B}"