changeset 19360 | f47412f922ab |
parent 17233 | 41eee2e7b465 |
19359:5d523a1b6ddc | 19360:f47412f922ab |
---|---|
1 (* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
1 (* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Mueller |
4 *) |
4 *) |
5 |
5 |
6 Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
6 Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
7 by Auto_tac; |
7 by Auto_tac; |
8 qed"compatibility_consequence3"; |
8 qed"compatibility_consequence3"; |