equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 LeadsTo relation, restricted to the set of reachable states. |
6 LeadsTo relation, restricted to the set of reachable states. |
7 *) |
7 *) |
8 |
|
9 overload_1st_set "SubstAx.op LeadsTo"; |
|
10 |
|
11 |
8 |
12 (*Resembles the previous definition of LeadsTo*) |
9 (*Resembles the previous definition of LeadsTo*) |
13 Goalw [LeadsTo_def] |
10 Goalw [LeadsTo_def] |
14 "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"; |
11 "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"; |
15 by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1); |
12 by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1); |