| changeset 5069 | 3ea049f7979d |
| parent 4776 | 1f9362e769c1 |
| child 5232 | e5a7cdd07ea5 |
--- a/src/HOL/UNITY/Network.ML Mon Jun 22 17:13:09 1998 +0200 +++ b/src/HOL/UNITY/Network.ML Mon Jun 22 17:26:46 1998 +0200 @@ -11,7 +11,7 @@ open Network; val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = -goalw thy [stable_def] +Goalw [stable_def] "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ \ !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ \ !! m proc. stable Acts {s. m <= s(proc,Sent)}; \