--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 26 12:18:51 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 26 16:37:56 1998 +0100
@@ -25,8 +25,7 @@
qed"Filter_actAisFilter_extA";
-(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A)
- or even better A||B= B||A, FIX *)
+(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
Goal "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
by Auto_tac;