| changeset 37936 | 1e4c5015a72e |
| parent 35417 | 47ee18b6ae32 |
| child 44106 | 0e018cbcc0de |
| 37935:7551769de556 | 37936:1e4c5015a72e |
|---|---|
1 (* Title: HOL/UNITY/SubstAx |
1 (* Title: HOL/UNITY/SubstAx.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 |
4 |
5 Weak LeadsTo relation (restricted to the set of reachable states) |
5 Weak LeadsTo relation (restricted to the set of reachable states) |
6 *) |
6 *) |