| changeset 58871 | c399ae4b836f |
| parent 57945 | cacb00a569e0 |
| child 58963 | 26bf09b95dda |
| 58870:e2c0d8ef29cb | 58871:c399ae4b836f |
|---|---|
3 Copyright 2001 University of Cambridge |
3 Copyright 2001 University of Cambridge |
4 |
4 |
5 Theory ported from HOL. |
5 Theory ported from HOL. |
6 *) |
6 *) |
7 |
7 |
8 header{*Weak LeadsTo relation (restricted to the set of reachable states)*} |
8 section{*Weak LeadsTo relation (restricted to the set of reachable states)*} |
9 |
9 |
10 theory SubstAx |
10 theory SubstAx |
11 imports WFair Constrains |
11 imports WFair Constrains |
12 begin |
12 begin |
13 |
13 |