changeset 2637 | e9b203f854ae |
parent 2520 | aecaa76e7eff |
child 2793 | b30c41754c86 |
2636:4b30dbe4a020 | 2637:e9b203f854ae |
---|---|
5 |
5 |
6 Equivalence of W and I. |
6 Equivalence of W and I. |
7 *) |
7 *) |
8 |
8 |
9 open I; |
9 open I; |
10 |
|
11 val op addss = op unsafe_addss; |
|
10 |
12 |
11 goal thy |
13 goal thy |
12 "! a m s s' t n. \ |
14 "! a m s s' t n. \ |
13 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
15 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
14 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |
16 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |