equal
deleted
inserted
replaced
4 |
4 |
5 Setup transitivity rules for calculational proofs. Note that in the |
5 Setup transitivity rules for calculational proofs. Note that in the |
6 list below later rules have priority. |
6 list below later rules have priority. |
7 *) |
7 *) |
8 |
8 |
9 theory Calculation = Int:; |
9 theory Calculation = IntArith:; |
10 |
10 |
11 theorems [trans] = rev_mp mp; |
11 theorems [trans] = rev_mp mp; |
12 |
12 |
13 theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *) |
13 theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *) |
14 by (rule ssubst); |
14 by (rule ssubst); |