src/HOLCF/IOA/meta_theory/Compositionality.ML

 *) 
 
 
 
 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
-by (Auto_tac());
+by Auto_tac;
 qed"compatibility_consequence3";
 
 
 goal thy 
 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \

 
 (* 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 *)
 
 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
-by (Auto_tac());
+by Auto_tac;
 qed"compatibility_consequence4";
 
 goal thy 
 "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
 \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";