changeset 16417 | 9bc16273c2d4 |
parent 15197 | 19e735596e51 |
child 16733 | 236dfafbeb63 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 |
5 |
6 Various examples. |
6 Various examples. |
7 *) |
7 *) |
8 |
8 |
9 theory Examples = Hoare + Arith2: |
9 theory Examples imports Hoare Arith2 begin |
10 |
10 |
11 (*** ARITHMETIC ***) |
11 (*** ARITHMETIC ***) |
12 |
12 |
13 (** multiplication by successive addition **) |
13 (** multiplication by successive addition **) |
14 |
14 |