| changeset 4477 | b3e5857d8d99 |
| parent 4423 | a129b817b58a |
| child 4559 | 8e604d885b54 |
| 4476:fbdc87f8ac7e | 4477:b3e5857d8d99 |
|---|---|
134 (* x is internal *) |
134 (* x is internal *) |
135 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
135 by (simp_tac (simpset() addcongs [conj_cong]) 1); |
136 by (rtac impI 1); |
136 by (rtac impI 1); |
137 by (etac conjE 1); |
137 by (etac conjE 1); |
138 by (forward_tac [reachable_rename] 1); |
138 by (forward_tac [reachable_rename] 1); |
139 by (Auto_tac()); |
139 by Auto_tac; |
140 qed"rename_through_pmap"; |
140 qed"rename_through_pmap"; |
141 |
141 |
142 |
142 |